awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
m : s.pt ⟶ (PullbackCone.mk a b comm).pt
m₁ : m ≫ (PullbackCone.mk a b comm).fst = s.fst
m₂ : m ≫ (PullbackCone.mk a b comm).snd = s.snd
refine_1 : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂
refine_2 :
  m ≫ PullbackCone.fst (PullbackCone.mk a b ⋯) =
    (IsPullback.isLimit big_k).lift s' ≫ PullbackCone.fst (PullbackCone.mk a b ⋯)
⊢ ∀ (j : WalkingCospan),
    m ≫ (IsPullback.cone big_k).π.app j = (IsPullback.isLimit big_k).lift s' ≫ (IsPullback.cone big_k).π.app j
have refine_3 : m ≫ PullbackCone.snd (PullbackCone.mk a b sorry) =
  (IsPullback.isLimit big_k).lift s' ≫ PullbackCone.snd (PullbackCone.mk a b sorry)
Tactic: refine (PullbackCone.mk a b ?_ : PullbackCone (f₁ ≫ f₂) _).equalizer_ext ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst_1 : Mono f₂
big_k : IsKernelPair (f₁ ≫ f₂) a b
⊢ a ≫ f₁ = b ≫ f₁
have rw : (a ≫ f₁) ≫ f₂ = (b ≫ f₁) ≫ f₂
Tactic: rw [← cancel_mono f₂, assoc, assoc, big_k.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst_1 : Mono f₂
big_k : IsKernelPair (f₁ ≫ f₂) a b
rw : (a ≫ f₁) ≫ f₂ = (b ≫ f₁) ≫ f₂
⊢ a ≫ f₁ = b ≫ f₁
have rw₁ : a ≫ f₁ ≫ f₂ = (b ≫ f₁) ≫ f₂
Tactic: rw [← cancel_mono f₂, assoc, assoc, big_k.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst_1 : Mono f₂
big_k : IsKernelPair (f₁ ≫ f₂) a b
rw : (a ≫ f₁) ≫ f₂ = (b ≫ f₁) ≫ f₂
rw₁ : a ≫ f₁ ≫ f₂ = (b ≫ f₁) ≫ f₂
⊢ a ≫ f₁ = b ≫ f₁
have rw₂ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂
Tactic: rw [← cancel_mono f₂, assoc, assoc, big_k.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst_1 : Mono f₂
big_k : IsKernelPair (f₁ ≫ f₂) a b
rw : (a ≫ f₁) ≫ f₂ = (b ≫ f₁) ≫ f₂
rw₁ : a ≫ f₁ ≫ f₂ = (b ≫ f₁) ≫ f₂
rw₂ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂
⊢ a ≫ f₁ = b ≫ f₁
have rw₃ : b ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂
Tactic: rw [← cancel_mono f₂, assoc, assoc, big_k.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst_1 : Mono f₂
small_k : IsKernelPair f₁ a b
⊢ a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂
have rw : b ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂
Tactic: rw [small_k.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst_1 : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
⊢ s.fst ≫ f₁ = s.snd ≫ f₁
have rw : (s.fst ≫ f₁) ≫ f₂ = (s.snd ≫ f₁) ≫ f₂
Tactic: rw [← cancel_mono f₂, assoc, s.condition, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst_1 : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
rw : (s.fst ≫ f₁) ≫ f₂ = (s.snd ≫ f₁) ≫ f₂
⊢ s.fst ≫ f₁ = s.snd ≫ f₁
have rw₁ : s.fst ≫ f₁ ≫ f₂ = (s.snd ≫ f₁) ≫ f₂
Tactic: rw [← cancel_mono f₂, assoc, s.condition, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst_1 : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
rw : (s.fst ≫ f₁) ≫ f₂ = (s.snd ≫ f₁) ≫ f₂
rw₁ : s.fst ≫ f₁ ≫ f₂ = (s.snd ≫ f₁) ≫ f₂
⊢ s.fst ≫ f₁ = s.snd ≫ f₁
have rw₂ : s.snd ≫ f₁ ≫ f₂ = (s.snd ≫ f₁) ≫ f₂
Tactic: rw [← cancel_mono f₂, assoc, s.condition, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst_1 : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
rw : (s.fst ≫ f₁) ≫ f₂ = (s.snd ≫ f₁) ≫ f₂
rw₁ : s.fst ≫ f₁ ≫ f₂ = (s.snd ≫ f₁) ≫ f₂
rw₂ : s.snd ≫ f₁ ≫ f₂ = (s.snd ≫ f₁) ≫ f₂
⊢ s.fst ≫ f₁ = s.snd ≫ f₁
have rw₃ : s.snd ≫ f₁ ≫ f₂ = s.snd ≫ f₁ ≫ f₂
Tactic: rw [← cancel_mono f₂, assoc, s.condition, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst_1 : Mono f₂
small_k : IsKernelPair f₁ a b
⊢ IsLimit (PullbackCone.mk a b ⋯)
have refine : ∀ (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) (m : s.pt ⟶ (PullbackCone.mk a b sorry).pt),
  (∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b sorry).π.app j = s.π.app j) →
    m = (fun (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) ↦ small_k.lift s.fst s.snd sorry) s
Tactic: refine PullbackCone.isLimitAux _
        (fun s => small_k.lift s.fst s.snd (by rw [← cancel_mono f₂, assoc, s.condition, assoc]))
        (by simp) (by simp) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst_1 : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt
hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j
⊢ m = (fun (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) ↦ small_k.lift s.fst s.snd ⋯) s
have apply : ∀ (j : WalkingCospan),
  m ≫ (IsPullback.cone small_k).π.app j =
    (fun (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) ↦ small_k.lift s.fst s.snd sorry) s ≫ (IsPullback.cone small_k).π.app j
Tactic: apply small_k.isLimit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst_1 : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt
hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j
⊢ ∀ (j : WalkingCospan),
    m ≫ (IsPullback.cone small_k).π.app j =
      (fun (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) ↦ small_k.lift s.fst s.snd ⋯) s ≫ (IsPullback.cone small_k).π.app j
have apply : m ≫ (IsPullback.cone small_k).fst =
  (fun (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) ↦ small_k.lift s.fst s.snd sorry) s ≫ (IsPullback.cone small_k).fst
Tactic: apply PullbackCone.equalizer_ext small_k.cone _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst_1 : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt
hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j
apply :
  m ≫ (IsPullback.cone small_k).fst =
    (fun (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) ↦ small_k.lift s.fst s.snd ⋯) s ≫ (IsPullback.cone small_k).fst
⊢ ∀ (j : WalkingCospan),
    m ≫ (IsPullback.cone small_k).π.app j =
      (fun (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) ↦ small_k.lift s.fst s.snd ⋯) s ≫ (IsPullback.cone small_k).π.app j
have apply₁ : m ≫ (IsPullback.cone small_k).snd =
  (fun (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) ↦ small_k.lift s.fst s.snd sorry) s ≫ (IsPullback.cone small_k).snd
Tactic: apply PullbackCone.equalizer_ext small_k.cone _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
⊢ IsColimit (Cofork.ofπ f ⋯)
have ht : t ≫ a = r.left
Tactic: have ht : t ≫ a = r.left := k.isLimit.fac _ WalkingCospan.left
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
ht : t ≫ a = r.left
⊢ IsColimit (Cofork.ofπ f ⋯)
have kt : t ≫ b = r.right
Tactic: have kt : t ≫ b = r.right := k.isLimit.fac _ WalkingCospan.right
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
ht : t ≫ a = r.left
kt : t ≫ b = r.right
s : Cofork a b
⊢ r.left ≫ s.π = r.right ≫ s.π
have rw : (t ≫ a) ≫ s.π = r.right ≫ s.π
Tactic: rw [← ht, assoc, s.condition, reassoc_of% kt]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
ht : t ≫ a = r.left
kt : t ≫ b = r.right
s : Cofork a b
rw : (t ≫ a) ≫ s.π = r.right ≫ s.π
⊢ r.left ≫ s.π = r.right ≫ s.π
have rw₁ : t ≫ a ≫ s.π = r.right ≫ s.π
Tactic: rw [← ht, assoc, s.condition, reassoc_of% kt]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
ht : t ≫ a = r.left
kt : t ≫ b = r.right
s : Cofork a b
rw : (t ≫ a) ≫ s.π = r.right ≫ s.π
rw₁ : t ≫ a ≫ s.π = r.right ≫ s.π
⊢ r.left ≫ s.π = r.right ≫ s.π
have rw₂ : t ≫ b ≫ s.π = r.right ≫ s.π
Tactic: rw [← ht, assoc, s.condition, reassoc_of% kt]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
ht : t ≫ a = r.left
kt : t ≫ b = r.right
s : Cofork a b
rw : (t ≫ a) ≫ s.π = r.right ≫ s.π
rw₁ : t ≫ a ≫ s.π = r.right ≫ s.π
rw₂ : t ≫ b ≫ s.π = r.right ≫ s.π
⊢ r.left ≫ s.π = r.right ≫ s.π
have rw₃ : r.right ≫ s.π = r.right ≫ s.π
Tactic: rw [← ht, assoc, s.condition, reassoc_of% kt]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
ht : t ≫ a = r.left
kt : t ≫ b = r.right
⊢ IsColimit (Cofork.ofπ f ⋯)
have refine_1 : ∀ (s : Cofork a b), (Cofork.ofπ f sorry).π ≫ (fun (s : Cofork a b) ↦ Cofork.IsColimit.desc r.isColimit s.π sorry) s = s.π
Tactic: refine Cofork.IsColimit.mk _
    (fun s => Cofork.IsColimit.desc r.isColimit s.π
      (by rw [← ht, assoc, s.condition, reassoc_of% kt]))
    (fun s => ?_) (fun s m w => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
ht : t ≫ a = r.left
kt : t ≫ b = r.right
refine_1 :
  ∀ (s : Cofork a b), (Cofork.ofπ f ⋯).π ≫ (fun (s : Cofork a b) ↦ Cofork.IsColimit.desc r.isColimit s.π ⋯) s = s.π
⊢ IsColimit (Cofork.ofπ f ⋯)
have refine_2 : ∀ (s : Cofork a b) (m : (Cofork.ofπ f sorry).pt ⟶ s.pt) (w : (Cofork.ofπ f sorry).π ≫ m = s.π),
  m = (fun (s : Cofork a b) ↦ Cofork.IsColimit.desc r.isColimit s.π sorry) s
Tactic: refine Cofork.IsColimit.mk _
    (fun s => Cofork.IsColimit.desc r.isColimit s.π
      (by rw [← ht, assoc, s.condition, reassoc_of% kt]))
    (fun s => ?_) (fun s m w => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
ht : t ≫ a = r.left
kt : t ≫ b = r.right
s : Cofork a b
m : (Cofork.ofπ f ⋯).pt ⟶ s.pt
w : (Cofork.ofπ f ⋯).π ≫ m = s.π
⊢ m = (fun (s : Cofork a b) ↦ Cofork.IsColimit.desc r.isColimit s.π ⋯) s
have refine_2 : (Cofork.ofπ f sorry).π ≫ m = (Cofork.ofπ f sorry).π ≫ (fun (s : Cofork a b) ↦ Cofork.IsColimit.desc r.isColimit s.π sorry) s
Tactic: apply Cofork.IsColimit.hom_ext r.isColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst_1 : HasPullback f g
inst_2 : HasPullback f (a₁ ≫ g)
⊢ Eq (α := pullback f (a₁ ≫ g) ⟶ X)
    (CategoryStruct.comp (Y := pullback f g) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.fst f g))
    (CategoryStruct.comp (Y := pullback f g) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) (pullback.fst f g))
have rw : Eq (α := pullback f (a₁ ≫ g) ⟶ X) (pullback.fst f (a₁ ≫ g) ≫ 𝟙 X)
  (CategoryStruct.comp (Y := pullback f g) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) sorry sorry) (pullback.fst f g))
Tactic: rw [pullback.lift_fst, pullback.lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst_1 : HasPullback f g
inst_2 : HasPullback f (a₁ ≫ g)
rw :
  Eq (α := pullback f (a₁ ≫ g) ⟶ X) (pullback.fst f (a₁ ≫ g) ≫ 𝟙 X)
    (CategoryStruct.comp (Y := pullback f g) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) (pullback.fst f g))
⊢ Eq (α := pullback f (a₁ ≫ g) ⟶ X)
    (CategoryStruct.comp (Y := pullback f g) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.fst f g))
    (CategoryStruct.comp (Y := pullback f g) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) (pullback.fst f g))
have rw₁ : Eq (α := pullback f (a₁ ≫ g) ⟶ X) (pullback.fst f (a₁ ≫ g) ≫ 𝟙 X) (pullback.fst f (a₁ ≫ g) ≫ 𝟙 X)
Tactic: rw [pullback.lift_fst, pullback.lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst_1 : HasPullback f g
inst_2 : HasPullback f (a₁ ≫ g)
⊢ IsKernelPair (R := pullback f (a₁ ≫ g)) (X := pullback f g) (pullback.fst f g)
    (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯)
have refine_1 : ∀ (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)),
  (s.fst ≫ pullback.snd f g) ≫ g = (s.snd ≫ pullback.snd f g) ≫ g
Tactic: refine ⟨⟨by rw [pullback.lift_fst, pullback.lift_fst]⟩, ⟨PullbackCone.isLimitAux _
    (fun s => pullback.lift (s.fst ≫ pullback.fst _ _)
      (h.lift (s.fst ≫ pullback.snd _ _) (s.snd ≫ pullback.snd _ _) ?_ ) ?_) (fun s => ?_)
        (fun s => ?_) (fun s (m : _ ⟶ pullback f (a₁ ≫ g)) hm => ?_)⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst_1 : HasPullback f g
inst_2 : HasPullback f (a₁ ≫ g)
refine_1 :
  ∀ (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)),
    (s.fst ≫ pullback.snd f g) ≫ g = (s.snd ≫ pullback.snd f g) ≫ g
⊢ IsKernelPair (R := pullback f (a₁ ≫ g)) (X := pullback f g) (pullback.fst f g)
    (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯)
have refine_2 : ∀ (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)),
  (s.fst ≫ pullback.fst f g) ≫ f = h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) sorry ≫ a₁ ≫ g
Tactic: refine ⟨⟨by rw [pullback.lift_fst, pullback.lift_fst]⟩, ⟨PullbackCone.isLimitAux _
    (fun s => pullback.lift (s.fst ≫ pullback.fst _ _)
      (h.lift (s.fst ≫ pullback.snd _ _) (s.snd ≫ pullback.snd _ _) ?_ ) ?_) (fun s => ?_)
        (fun s => ?_) (fun s (m : _ ⟶ pullback f (a₁ ≫ g)) hm => ?_)⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst_1 : HasPullback f g
inst_2 : HasPullback f (a₁ ≫ g)
refine_1 :
  ∀ (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)),
    (s.fst ≫ pullback.snd f g) ≫ g = (s.snd ≫ pullback.snd f g) ≫ g
refine_2 :
  ∀ (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)),
    (s.fst ≫ pullback.fst f g) ≫ f = h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯ ≫ a₁ ≫ g
⊢ IsKernelPair (R := pullback f (a₁ ≫ g)) (X := pullback f g) (pullback.fst f g)
    (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯)
have refine_3 : ∀ (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)),
  CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g))
        (PullbackCone.mk (W := pullback f (a₁ ≫ g)) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) sorry sorry)
          (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) sorry sorry) sorry))
      ((fun (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)) ↦
          (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) sorry) sorry :
            s.pt ⟶ pullback f (a₁ ≫ g)))
        s)
      (PullbackCone.fst
        (PullbackCone.mk (W := pullback f (a₁ ≫ g)) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) sorry sorry)
          (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) sorry sorry) sorry)) =
    s.fst
Tactic: refine ⟨⟨by rw [pullback.lift_fst, pullback.lift_fst]⟩, ⟨PullbackCone.isLimitAux _
    (fun s => pullback.lift (s.fst ≫ pullback.fst _ _)
      (h.lift (s.fst ≫ pullback.snd _ _) (s.snd ≫ pullback.snd _ _) ?_ ) ?_) (fun s => ?_)
        (fun s => ?_) (fun s (m : _ ⟶ pullback f (a₁ ≫ g)) hm => ?_)⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst_1 : HasPullback f g
inst_2 : HasPullback f (a₁ ≫ g)
refine_1 :
  ∀ (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)),
    (s.fst ≫ pullback.snd f g) ≫ g = (s.snd ≫ pullback.snd f g) ≫ g
refine_2 :
  ∀ (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)),
    (s.fst ≫ pullback.fst f g) ≫ f = h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯ ≫ a₁ ≫ g
refine_3 :
  ∀ (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)),
    CategoryStruct.comp (Y :=
        Cone.pt (F := cospan (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g))
          (PullbackCone.mk (W := pullback f (a₁ ≫ g)) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯))
        ((fun (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)) ↦
            (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯)
                ⋯ :
              s.pt ⟶ pullback f (a₁ ≫ g)))
          s)
        (PullbackCone.fst
          (PullbackCone.mk (W := pullback f (a₁ ≫ g)) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯)) =
      s.fst
⊢ IsKernelPair (R := pullback f (a₁ ≫ g)) (X := pullback f g) (pullback.fst f g)
    (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯)
have refine_4 : ∀ (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)),
  CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g))
        (PullbackCone.mk (W := pullback f (a₁ ≫ g)) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) sorry sorry)
          (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) sorry sorry) sorry))
      ((fun (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)) ↦
          (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) sorry) sorry :
            s.pt ⟶ pullback f (a₁ ≫ g)))
        s)
      (PullbackCone.snd
        (PullbackCone.mk (W := pullback f (a₁ ≫ g)) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) sorry sorry)
          (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) sorry sorry) sorry)) =
    s.snd
Tactic: refine ⟨⟨by rw [pullback.lift_fst, pullback.lift_fst]⟩, ⟨PullbackCone.isLimitAux _
    (fun s => pullback.lift (s.fst ≫ pullback.fst _ _)
      (h.lift (s.fst ≫ pullback.snd _ _) (s.snd ≫ pullback.snd _ _) ?_ ) ?_) (fun s => ?_)
        (fun s => ?_) (fun s (m : _ ⟶ pullback f (a₁ ≫ g)) hm => ?_)⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst_1 : HasPullback f g
inst_2 : HasPullback f (a₁ ≫ g)
s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)
⊢ (s.fst ≫ pullback.snd f g) ≫ g = (s.snd ≫ pullback.snd f g) ≫ g
have refine_1 : s.fst ≫ pullback.snd f g ≫ g = s.snd ≫ pullback.snd f g ≫ g
Tactic: simp_rw [Category.assoc, ← pullback.condition, ← Category.assoc, s.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst_1 : HasPullback f g
inst_2 : HasPullback f (a₁ ≫ g)
s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)
refine_1 : s.fst ≫ pullback.snd f g ≫ g = s.snd ≫ pullback.snd f g ≫ g
⊢ (s.fst ≫ pullback.snd f g) ≫ g = (s.snd ≫ pullback.snd f g) ≫ g
have refine_1₁ : s.fst ≫ pullback.fst f g ≫ f = s.snd ≫ pullback.fst f g ≫ f
Tactic: simp_rw [Category.assoc, ← pullback.condition, ← Category.assoc, s.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst_1 : HasPullback f g
inst_2 : HasPullback f (a₁ ≫ g)
s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)
refine_1 : s.fst ≫ pullback.snd f g ≫ g = s.snd ≫ pullback.snd f g ≫ g
refine_1₁ : s.fst ≫ pullback.fst f g ≫ f = s.snd ≫ pullback.fst f g ≫ f
⊢ (s.fst ≫ pullback.snd f g) ≫ g = (s.snd ≫ pullback.snd f g) ≫ g
have refine_1₂ : (s.fst ≫ pullback.fst f g) ≫ f = (s.snd ≫ pullback.fst f g) ≫ f
Tactic: simp_rw [Category.assoc, ← pullback.condition, ← Category.assoc, s.condition]