awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
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) ⋯
⊢ Eq (α := (span f g).obj (some WalkingPair.right) ⟶ s.pt)
    (NatTrans.app
          (Cocone.ι
            (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair })
              (c.ι.app { as := WalkingPair.right }) ⋯))
          (some WalkingPair.right) ≫
        m :
      (span f g).obj (some WalkingPair.right) ⟶ s.pt)
    (CategoryStruct.comp (Y :=
        Functor.obj.{0, v, 0, u}
          (Functor.obj (Functor.const WalkingSpan)
            (Cocone.pt (F := span f g)
              (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair })
                  (c.ι.app { as := WalkingPair.right : Discrete WalkingPair }) ⋯ :
                PushoutCocone f g)))
          (some WalkingPair.right))
        (NatTrans.app
          (Cocone.ι
            (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair })
              (c.ι.app { as := WalkingPair.right }) ⋯))
          (some WalkingPair.right))
        (hc.desc
          (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
            (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)) :
      (span f g).obj (some WalkingPair.right) ⟶ s.pt)
have some : Eq (α := (span f g).obj (some WalkingPair.right) ⟶ s.pt) (c.ι.app { as := WalkingPair.right } ≫ m)
  (c.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫
    hc.desc
      (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
        (c.ι.app { as := WalkingPair.right } ≫ m) sorry))
Tactic: simp only [PushoutCocone.mk_ι_app, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
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) ⋯
⊢ f ≫ c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m =
    f ≫
      c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
        hc.desc
          (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
            (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)
have none : Eq (α := F.obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt) (c.ι.app { as := WalkingPair.left } ≫ m)
  (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
    hc.desc
      (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
        (c.ι.app { as := WalkingPair.right } ≫ m) sorry))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
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) ⋯
⊢ f ≫ c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m =
    f ≫
      c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
        hc.desc
          (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
            (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)
have none : Eq (α := F.obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt) (c.ι.app { as := WalkingPair.left } ≫ m)
  (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
    hc.desc
      (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
        (c.ι.app { as := WalkingPair.right } ≫ m) sorry))
Tactic: on_goal 1 => congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
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₁ : IsInitial.{v, u} W
H₂ : IsColimit (F := span h k) (PushoutCocone.mk f g ⋯)
⊢ IsColimit (BinaryCofan.mk f g)
have hc : IsColimit (F := span h k)
  (PushoutCocone.mk ((BinaryCofan.mk f g).ι.app { as := WalkingPair.left : Discrete WalkingPair })
      ((BinaryCofan.mk f g).ι.app { as := WalkingPair.right }) sorry :
    PushoutCocone h k)
Tactic: apply isBinaryCoproductOfIsInitialIsPushout _ _ H₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
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₁ : IsInitial.{v, u} W
H₂ : IsColimit (F := span h k) (PushoutCocone.mk f g ⋯)
hc :
  IsColimit (F := span h k)
    (PushoutCocone.mk ((BinaryCofan.mk f g).ι.app { as := WalkingPair.left : Discrete WalkingPair })
        ((BinaryCofan.mk f g).ι.app { as := WalkingPair.right }) ⋯ :
      PushoutCocone h k)
⊢ IsColimit (BinaryCofan.mk f g)
have f₁ : W ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }
Tactic: apply isBinaryCoproductOfIsInitialIsPushout _ _ H₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
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₁ : IsInitial.{v, u} W
H₂ : IsColimit (F := span h k) (PushoutCocone.mk f g ⋯)
hc :
  IsColimit (F := span h k)
    (PushoutCocone.mk ((BinaryCofan.mk f g).ι.app { as := WalkingPair.left : Discrete WalkingPair })
        ((BinaryCofan.mk f g).ι.app { as := WalkingPair.right }) ⋯ :
      PushoutCocone h k)
f₁ : W ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }
⊢ IsColimit (BinaryCofan.mk f g)
have g₁ : W ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }
Tactic: apply isBinaryCoproductOfIsInitialIsPushout _ _ H₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
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₁ : IsInitial.{v, u} W
H₂ : IsColimit (BinaryCofan.mk f g)
⊢ IsColimit (F := span h k) (PushoutCocone.mk f g ⋯)
have create : (s : PushoutCocone h k) →
  { l : Cocone.pt (F := span h k) (PushoutCocone.mk f g sorry) ⟶ s.pt //
    PushoutCocone.inl (PushoutCocone.mk f g sorry) ≫ l = s.inl ∧
      PushoutCocone.inr (PushoutCocone.mk f g sorry) ≫ l = s.inr ∧
        ∀ {m : Cocone.pt (F := span h k) (PushoutCocone.mk f g sorry) ⟶ s.pt},
          PushoutCocone.inl (PushoutCocone.mk f g sorry) ≫ m = s.inl →
            PushoutCocone.inr (PushoutCocone.mk f g sorry) ≫ m = s.inr → m = l }
Tactic: apply PushoutCocone.isColimitAux'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
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₁ : IsInitial.{v, u} W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
⊢ { l : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt //
    PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ l = s.inl ∧
      PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ l = s.inr ∧
        ∀ {m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt},
          PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl →
            PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr → m = l }
have property : PushoutCocone.inl (PushoutCocone.mk f g sorry) ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr = s.inl ∧
  PushoutCocone.inr (PushoutCocone.mk f g sorry) ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr = s.inr ∧
    ∀ {m : Cocone.pt (F := span h k) (PushoutCocone.mk f g sorry) ⟶ s.pt},
      PushoutCocone.inl (PushoutCocone.mk f g sorry) ≫ m = s.inl →
        PushoutCocone.inr (PushoutCocone.mk f g sorry) ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr
Tactic: use BinaryCofan.IsColimit.desc H₂ s.inl s.inr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
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₁ : IsInitial.{v, u} W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
⊢ PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr = s.inl ∧
    PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr = s.inr ∧
      ∀ {m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt},
        PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl →
          PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr
have right : PushoutCocone.inr (PushoutCocone.mk f g sorry) ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr = s.inr ∧
  ∀ {m : Cocone.pt (F := span h k) (PushoutCocone.mk f g sorry) ⟶ s.pt},
    PushoutCocone.inl (PushoutCocone.mk f g sorry) ≫ m = s.inl →
      PushoutCocone.inr (PushoutCocone.mk f g sorry) ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr
Tactic: use BinaryCofan.IsColimit.inl_desc H₂ _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
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₁ : IsInitial.{v, u} W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
⊢ PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr = s.inr ∧
    ∀ {m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt},
      PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl →
        PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr
have right : ∀ {m : Cocone.pt (F := span h k) (PushoutCocone.mk f g sorry) ⟶ s.pt},
  PushoutCocone.inl (PushoutCocone.mk f g sorry) ≫ m = s.inl →
    PushoutCocone.inr (PushoutCocone.mk f g sorry) ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr
Tactic: use BinaryCofan.IsColimit.inr_desc H₂ _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
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₁ : IsInitial.{v, u} W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt
h₁ : PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl
h₂ : PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr
⊢ m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr
have right : ∀ (j : Discrete WalkingPair),
  (BinaryCofan.mk f g).ι.app j ≫ m = (BinaryCofan.mk f g).ι.app j ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr
Tactic: apply H₂.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
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 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst_5 : PreservesColimitsOfShape WalkingSpan F
K : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
⊢ IsColimit (F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone)
have hc : IsColimit (F :=
  span (X := F.obj (initial.{v, u} C)) (F.map (initial.to (K.obj { as := WalkingPair.left })))
    (F.map (initial.to (K.obj { as := WalkingPair.right }))))
  (PushoutCocone.mk
      ((F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone).ι.app
        { as := WalkingPair.left : Discrete WalkingPair })
      ((F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone).ι.app { as := WalkingPair.right }) sorry :
    PushoutCocone (X := F.obj (initial.{v, u} C)) (F.map (initial.to (K.obj { as := WalkingPair.left })))
      (F.map (initial.to (K.obj { as := WalkingPair.right }))))
Tactic: apply
        isBinaryCoproductOfIsInitialIsPushout _ _
          (isColimitOfHasInitialOfPreservesColimit F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
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 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst_5 : PreservesColimitsOfShape WalkingSpan F
K : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
hc :
  IsColimit (F :=
    span (X := F.obj (initial.{v, u} C)) (F.map (initial.to (K.obj { as := WalkingPair.left })))
      (F.map (initial.to (K.obj { as := WalkingPair.right }))))
    (PushoutCocone.mk
        ((F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone).ι.app
          { as := WalkingPair.left : Discrete WalkingPair })
        ((F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone).ι.app { as := WalkingPair.right }) ⋯ :
      PushoutCocone (X := F.obj (initial.{v, u} C)) (F.map (initial.to (K.obj { as := WalkingPair.left })))
        (F.map (initial.to (K.obj { as := WalkingPair.right }))))
⊢ IsColimit (F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone)
have f : F.obj (initial.{v, u} C) ⟶ (K ⋙ F).obj { as := WalkingPair.left }
Tactic: apply
        isBinaryCoproductOfIsInitialIsPushout _ _
          (isColimitOfHasInitialOfPreservesColimit F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
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 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst_5 : PreservesColimitsOfShape WalkingSpan F
K : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
hc :
  IsColimit (F :=
    span (X := F.obj (initial.{v, u} C)) (F.map (initial.to (K.obj { as := WalkingPair.left })))
      (F.map (initial.to (K.obj { as := WalkingPair.right }))))
    (PushoutCocone.mk
        ((F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone).ι.app
          { as := WalkingPair.left : Discrete WalkingPair })
        ((F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone).ι.app { as := WalkingPair.right }) ⋯ :
      PushoutCocone (X := F.obj (initial.{v, u} C)) (F.map (initial.to (K.obj { as := WalkingPair.left })))
        (F.map (initial.to (K.obj { as := WalkingPair.right }))))
f : F.obj (initial.{v, u} C) ⟶ (K ⋙ F).obj { as := WalkingPair.left }
⊢ IsColimit (F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone)
have g : F.obj (initial.{v, u} C) ⟶ (K ⋙ F).obj { as := WalkingPair.right }
Tactic: apply
        isBinaryCoproductOfIsInitialIsPushout _ _
          (isColimitOfHasInitialOfPreservesColimit F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EpiMono (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : PreservesLimit (cospan f f) F
inst_3 : Mono f
⊢ Mono (F.map f)
have have : ∀
  (this :
    have this : F.map (𝟙 X) ≫ F.map f = F.map (𝟙 X) ≫ F.map f := sorry;
    IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) this)),
  Mono (F.map f)
Tactic: have := isLimitPullbackConeMapOfIsLimit F _ (PullbackCone.isLimitMkIdId f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EpiMono (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : PreservesLimit (cospan f f) F
inst_3 : Mono f
this :
  have this : F.map (𝟙 X) ≫ F.map f = F.map (𝟙 X) ≫ F.map f := ⋯;
  IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) this)
⊢ Mono (F.map f)
have simp_rw : ∀ (this : IsLimit (F := cospan (F.map f) (F.map f)) (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) sorry)), Mono (F.map f)
Tactic: simp_rw [F.map_id] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EpiMono (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : ReflectsLimit (cospan f f) F
inst_3 : Mono (F.map f)
⊢ Mono f
have have : ∀ (this : IsLimit.{0, v₂, 0, u₂} (F := cospan (F.map f) (F.map f)) (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) sorry)),
  Mono f
Tactic: have := PullbackCone.isLimitMkIdId (F.map f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EpiMono (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : ReflectsLimit (cospan f f) F
inst_3 : Mono (F.map f)
this : IsLimit.{0, v₂, 0, u₂} (F := cospan (F.map f) (F.map f)) (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)
⊢ Mono f
have simp_rw : ∀ (this : IsLimit (F := cospan (F.map f) (F.map f)) (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) sorry)), Mono f
Tactic: simp_rw [← F.map_id] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EpiMono (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : PreservesColimit (span f f) F
inst_3 : Epi f
⊢ Epi (F.map f)
have have : ∀ (this : IsColimit (F := span (F.map f) (F.map f)) (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) sorry)), Epi (F.map f)
Tactic: have := isColimitPushoutCoconeMapOfIsColimit F _ (PushoutCocone.isColimitMkIdId f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EpiMono (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : PreservesColimit (span f f) F
inst_3 : Epi f
this : IsColimit (F := span (F.map f) (F.map f)) (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)
⊢ Epi (F.map f)
have simp_rw : ∀ (this : IsColimit.{0, v₂, 0, u₂} (F := span (F.map f) (F.map f)) (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) sorry)),
  Epi (F.map f)
Tactic: simp_rw [F.map_id] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EpiMono (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : ReflectsColimit (span f f) F
inst_3 : Epi (F.map f)
⊢ Epi f
have have : ∀ (this : IsColimit.{0, v₂, 0, u₂} (F := span (F.map f) (F.map f)) (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) sorry)),
  Epi f
Tactic: have := PushoutCocone.isColimitMkIdId (F.map f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EpiMono (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : ReflectsColimit (span f f) F
inst_3 : Epi (F.map f)
this : IsColimit.{0, v₂, 0, u₂} (F := span (F.map f) (F.map f)) (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) ⋯)
⊢ Epi f
have simp_rw : ∀ (this : IsColimit (F := span (F.map f) (F.map f)) (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) sorry)), Epi f
Tactic: simp_rw [← F.map_id] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.zero) (pullbackFst F)
    (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)))
have h : Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.zero) (pullbackFst F)
  (CategoryStruct.comp (Y := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
    (pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
    prod.fst)
Tactic: convert!
    (eq_whisker pullback.condition Limits.prod.fst :
      (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.zero) = _)