awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (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
X Y Z : C
f_1 : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ Eq (α := (span f_1 g ⋙ F).obj (some WalkingPair.right) ⟶ (span (F.map f_1) (F.map g)).obj (some WalkingPair.right))
    ((span f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.right) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.right) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (F.map f_1) (F.map g)).map f)
have some : Eq (α := (span f_1 g ⋙ F).obj (some WalkingPair.right) ⟶ (span (F.map f_1) (F.map g)).obj (some WalkingPair.right))
  ((span f_1 g ⋙ F).map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
    Iso.hom
      (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
        (some WalkingPair.right) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
  (Iso.hom
      (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
        (some WalkingPair.right) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
    (span (F.map f_1) (F.map g)).map (WidePushoutShape.Hom.id (some WalkingPair.right)))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
⊢ Eq (α := equalizer f g ⟶ prod.{v, u} Y Y) (equalizer.ι f g ≫ prod.lift f g)
    ((equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y))
have h₁ : Eq (α := equalizer f g ⟶ Y) (CategoryStruct.comp (Y := prod.{v, u} Y Y) (equalizer.ι f g ≫ prod.lift f g) prod.fst)
  (CategoryStruct.comp (Y := prod.{v, u} Y Y) ((equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y)) prod.fst)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
h₁ :
  Eq (α := equalizer f g ⟶ Y) (CategoryStruct.comp (Y := prod.{v, u} Y Y) (equalizer.ι f g ≫ prod.lift f g) prod.fst)
    (CategoryStruct.comp (Y := prod.{v, u} Y Y) ((equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y)) prod.fst)
⊢ Eq (α := equalizer f g ⟶ prod.{v, u} Y Y) (equalizer.ι f g ≫ prod.lift f g)
    ((equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y))
have h₂ : Eq (α := equalizer f g ⟶ Y) (CategoryStruct.comp (Y := prod.{v, u} Y Y) (equalizer.ι f g ≫ prod.lift f g) prod.snd)
  (CategoryStruct.comp (Y := prod.{v, u} Y Y) ((equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y)) prod.snd)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
⊢ IsPullback (P := equalizer f g) (Z := prod.{v, u} Y Y) (equalizer.ι f g) (equalizer.ι f g ≫ f) (prod.lift f g)
    (prod.lift (𝟙 Y) (𝟙 Y))
have refine_1 : (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))) → s.pt ⟶ equalizer f g
Tactic: refine ⟨⟨by ext <;> simp [equalizer.condition f g]⟩, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
refine_1 : (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))) → s.pt ⟶ equalizer f g
⊢ IsPullback (P := equalizer f g) (Z := prod.{v, u} Y Y) (equalizer.ι f g) (equalizer.ι f g ≫ f) (prod.lift f g)
    (prod.lift (𝟙 Y) (𝟙 Y))
have refine_2 : ∀ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))),
  CategoryStruct.comp (Y := equalizer f g) (equalizer.lift s.fst sorry) (equalizer.ι f g) = s.fst
Tactic: refine ⟨⟨by ext <;> simp [equalizer.condition f g]⟩, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
refine_1 : (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))) → s.pt ⟶ equalizer f g
refine_2 :
  ∀ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))),
    CategoryStruct.comp (Y := equalizer f g) (equalizer.lift s.fst ⋯) (equalizer.ι f g) = s.fst
⊢ IsPullback (P := equalizer f g) (Z := prod.{v, u} Y Y) (equalizer.ι f g) (equalizer.ι f g ≫ f) (prod.lift f g)
    (prod.lift (𝟙 Y) (𝟙 Y))
have refine_3 : ∀ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))),
  CategoryStruct.comp (Y := equalizer f g) (equalizer.lift s.fst sorry) (equalizer.ι f g ≫ f) = s.snd
Tactic: refine ⟨⟨by ext <;> simp [equalizer.condition f g]⟩, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
refine_1 : (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))) → s.pt ⟶ equalizer f g
refine_2 :
  ∀ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))),
    CategoryStruct.comp (Y := equalizer f g) (equalizer.lift s.fst ⋯) (equalizer.ι f g) = s.fst
refine_3 :
  ∀ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))),
    CategoryStruct.comp (Y := equalizer f g) (equalizer.lift s.fst ⋯) (equalizer.ι f g ≫ f) = s.snd
⊢ IsPullback (P := equalizer f g) (Z := prod.{v, u} Y Y) (equalizer.ι f g) (equalizer.ι f g ≫ f) (prod.lift f g)
    (prod.lift (𝟙 Y) (𝟙 Y))
have refine_4 : ∀ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))) (m : s.pt ⟶ equalizer f g),
  m ≫ equalizer.ι f g = s.fst → m ≫ equalizer.ι f g ≫ f = s.snd → m = equalizer.lift s.fst sorry
Tactic: refine ⟨⟨by ext <;> simp [equalizer.condition f g]⟩, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
⊢ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))) → s.pt ⟶ equalizer f g
have refine_1 : ∀ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))), s.fst ≫ f = s.fst ≫ g
Tactic: refine fun s ↦ equalizer.lift s.fst ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
⊢ s.fst ≫ f = s.fst ≫ g
have H₁ : s.fst ≫ f = s.snd
Tactic: have H₁ : s.fst ≫ f = s.snd := by simpa using congr($s.condition ≫ prod.fst)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
H₁ : s.fst ≫ f = s.snd
⊢ s.fst ≫ f = s.fst ≫ g
have H₂ : s.fst ≫ g = s.snd
Tactic: have H₂ : s.fst ≫ g = s.snd := by simpa using congr($s.condition ≫ prod.snd)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
m : s.pt ⟶ equalizer f g
hm : m ≫ equalizer.ι f g = s.fst
h : m ≫ equalizer.ι f g ≫ f = s.snd
⊢ m = equalizer.lift s.fst ⋯
have h : m ≫ equalizer.ι f g = CategoryStruct.comp (Y := equalizer f g) (equalizer.lift s.fst sorry) (equalizer.ι f g)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
⊢ Eq (α := coprod.{v, u} X X ⟶ coequalizer f g) (coprod.desc f g ≫ coequalizer.π f g)
    (coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π f g)
have h₁ : Eq (α := X ⟶ coequalizer f g)
  (CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (coprod.desc f g ≫ coequalizer.π f g))
  (CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π f g))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
h₁ :
  Eq (α := X ⟶ coequalizer f g)
    (CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (coprod.desc f g ≫ coequalizer.π f g))
    (CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π f g))
⊢ Eq (α := coprod.{v, u} X X ⟶ coequalizer f g) (coprod.desc f g ≫ coequalizer.π f g)
    (coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π f g)
have h₂ : Eq (α := X ⟶ coequalizer f g)
  (CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (coprod.desc f g ≫ coequalizer.π f g))
  (CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π f g))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
⊢ IsPushout (Z := coprod.{v, u} X X) (P := coequalizer f g) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
    (coequalizer.π f g) (f ≫ coequalizer.π f g)
have refine_1 : (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))) → coequalizer f g ⟶ s.pt
Tactic: refine ⟨⟨by ext <;> simp [coequalizer.condition f g]⟩, ⟨PushoutCocone.IsColimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
refine_1 :
  (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))) → coequalizer f g ⟶ s.pt
⊢ IsPushout (Z := coprod.{v, u} X X) (P := coequalizer f g) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
    (coequalizer.π f g) (f ≫ coequalizer.π f g)
have refine_2 : ∀ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))),
  CategoryStruct.comp (Y := coequalizer f g) (coequalizer.π f g) (coequalizer.desc s.inl sorry) = s.inl
Tactic: refine ⟨⟨by ext <;> simp [coequalizer.condition f g]⟩, ⟨PushoutCocone.IsColimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
refine_1 :
  (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))) → coequalizer f g ⟶ s.pt
refine_2 :
  ∀ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))),
    CategoryStruct.comp (Y := coequalizer f g) (coequalizer.π f g) (coequalizer.desc s.inl ⋯) = s.inl
⊢ IsPushout (Z := coprod.{v, u} X X) (P := coequalizer f g) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
    (coequalizer.π f g) (f ≫ coequalizer.π f g)
have refine_3 : ∀ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))),
  CategoryStruct.comp (Y := coequalizer f g) (f ≫ coequalizer.π f g) (coequalizer.desc s.inl sorry) = s.inr
Tactic: refine ⟨⟨by ext <;> simp [coequalizer.condition f g]⟩, ⟨PushoutCocone.IsColimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
refine_1 :
  (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))) → coequalizer f g ⟶ s.pt
refine_2 :
  ∀ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))),
    CategoryStruct.comp (Y := coequalizer f g) (coequalizer.π f g) (coequalizer.desc s.inl ⋯) = s.inl
refine_3 :
  ∀ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))),
    CategoryStruct.comp (Y := coequalizer f g) (f ≫ coequalizer.π f g) (coequalizer.desc s.inl ⋯) = s.inr
⊢ IsPushout (Z := coprod.{v, u} X X) (P := coequalizer f g) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
    (coequalizer.π f g) (f ≫ coequalizer.π f g)
have refine_4 : ∀ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))) (m : coequalizer f g ⟶ s.pt),
  coequalizer.π f g ≫ m = s.inl → (f ≫ coequalizer.π f g) ≫ m = s.inr → m = coequalizer.desc s.inl sorry
Tactic: refine ⟨⟨by ext <;> simp [coequalizer.condition f g]⟩, ⟨PushoutCocone.IsColimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
⊢ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))) → coequalizer f g ⟶ s.pt
have refine_1 : ∀ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))), f ≫ s.inl = g ≫ s.inl
Tactic: refine fun s ↦ coequalizer.desc s.inl ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ f ≫ s.inl = g ≫ s.inl
have H₁ : f ≫ s.inl = s.inr
Tactic: have H₁ : f ≫ s.inl = s.inr := by simpa using congr(coprod.inl ≫ $s.condition)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
H₁ : f ≫ s.inl = s.inr
⊢ f ≫ s.inl = g ≫ s.inl
have H₂ : g ≫ s.inl = s.inr
Tactic: have H₂ : g ≫ s.inl = s.inr := by simpa using congr(coprod.inr ≫ $s.condition)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
m : coequalizer f g ⟶ s.pt
hm : coequalizer.π f g ≫ m = s.inl
h : (f ≫ coequalizer.π f g) ≫ m = s.inr
⊢ m = coequalizer.desc s.inl ⋯
have h : coequalizer.π f g ≫ m = CategoryStruct.comp (Y := coequalizer f g) (coequalizer.π f g) (coequalizer.desc s.inl sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback t v)
    (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ lhs)
    (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ rhs)
have h₀ : Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ Y)
  ((pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s sorry sorry ≫ lhs) ≫
    pullback.fst t v)
  ((pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s sorry sorry ≫ rhs) ≫
    pullback.fst t v)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
h₀ :
  Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ Y)
    ((pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ lhs) ≫
      pullback.fst t v)
    ((pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ rhs) ≫
      pullback.fst t v)
⊢ Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback t v)
    (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ lhs)
    (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ rhs)
have h₁ : Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ T)
  ((pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s sorry sorry ≫ lhs) ≫
    pullback.snd t v)
  ((pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s sorry sorry ≫ rhs) ≫
    pullback.snd t v)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ CategoryStruct.comp (Y := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
      (pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
        (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯)
      (equalizer.lift (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯)
        ⋯) =
    𝟙 (equalizer lhs rhs)
have h : CategoryStruct.comp (Y := equalizer lhs rhs)
      (CategoryStruct.comp (Y := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
        (pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) sorry)
          (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) sorry) sorry)
        (equalizer.lift
          (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s sorry sorry) sorry))
      (equalizer.ι lhs rhs) ≫
    pullback.fst s v =
  (𝟙 (equalizer lhs rhs) ≫ equalizer.ι lhs rhs) ≫ pullback.fst s v
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
h :
  CategoryStruct.comp (Y := equalizer lhs rhs)
        (CategoryStruct.comp (Y :=
          pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
          (pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
            (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯)
          (equalizer.lift
            (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯) ⋯))
        (equalizer.ι lhs rhs) ≫
      pullback.fst s v =
    (𝟙 (equalizer lhs rhs) ≫ equalizer.ι lhs rhs) ≫ pullback.fst s v
⊢ CategoryStruct.comp (Y := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
      (pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
        (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯)
      (equalizer.lift (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯)
        ⋯) =
    𝟙 (equalizer lhs rhs)
have h₁ : CategoryStruct.comp (Y := equalizer lhs rhs)
      (CategoryStruct.comp (Y := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v))
        (pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) sorry)
          (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) sorry) sorry)
        (equalizer.lift
          (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s sorry sorry) sorry))
      (equalizer.ι lhs rhs) ≫
    pullback.snd s v =
  (𝟙 (equalizer lhs rhs) ≫ equalizer.ι lhs rhs) ≫ pullback.snd s v
Tactic: ext