awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
P Q : IsKernelPair f a b
⊢ P = Q

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
⊢ IsKernelPair f (𝟙 X) (𝟙 X)

Tactic:
⟨⟨rfl⟩, ⟨PullbackCone.isLimitMkIdId _⟩⟩

Premises used: CategoryTheory.Limits.PullbackCone.isLimitMkIdId, CategoryTheory.IsPullback.mk, CategoryTheory.CommSq.mk, Nonempty.intro, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
S : C
k : IsKernelPair f a b
p q : S ⟶ X
w : p ≫ f = q ≫ f
⊢ k.lift p q w ≫ a = p

Tactic:
PullbackCone.IsLimit.lift_fst _ _ _ _

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst, CategoryTheory.IsKernelPair.lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
S : C
k : IsKernelPair f a b
p q : S ⟶ X
w : p ≫ f = q ≫ f
⊢ k.lift p q w ≫ b = q

Tactic:
PullbackCone.IsLimit.lift_snd _ _ _ _

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd, CategoryTheory.IsKernelPair.lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
S : C
k : IsKernelPair f a b
p q : S ⟶ X
w : p ≫ f = q ≫ f
⊢ k.lift p q w ≫ a = p ∧ k.lift p q w ≫ b = q

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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 ⋯
refine :
  ∀ {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), m = (IsPullback.isLimit big_k).lift s'
⊢ { l : s.pt ⟶ (PullbackCone.mk a b comm).pt //
    l ≫ (PullbackCone.mk a b comm).fst = s.fst ∧
      l ≫ (PullbackCone.mk a b comm).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk a b comm).pt},
          m ≫ (PullbackCone.mk a b comm).fst = s.fst → m ≫ (PullbackCone.mk a b comm).snd = s.snd → m = l }

Tactic:
refine ⟨big_k.isLimit.lift s', big_k.isLimit.fac _ WalkingCospan.left,
          big_k.isLimit.fac _ WalkingCospan.right, fun m₁ m₂ => ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
apply :
  ∀ (j : WalkingCospan),
    m ≫ (IsPullback.cone big_k).π.app j = (IsPullback.isLimit big_k).lift s' ≫ (IsPullback.cone big_k).π.app j
⊢ m = (IsPullback.isLimit big_k).lift s'

Tactic:
apply big_k.isLimit.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
⊢ ∀ (j : WalkingCospan),
    m ≫ (IsPullback.cone big_k).π.app j = (IsPullback.isLimit big_k).lift s' ≫ (IsPullback.cone big_k).π.app j

Tactic:
(PullbackCone.mk a b ?_ : PullbackCone (f₁ ≫ f₂) _).equalizer_ext ?_ ?_

Premises used: CategoryTheory.Limits.PullbackCone.mk, CategoryTheory.Limits.PullbackCone.equalizer_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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 ⋯)
refine_3 :
  m ≫ PullbackCone.snd (PullbackCone.mk a b ⋯) =
    (IsPullback.isLimit big_k).lift s' ≫ PullbackCone.snd (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

Tactic:
refine (PullbackCone.mk a b ?_ : PullbackCone (f₁ ≫ f₂) _).equalizer_ext ?_ ?_

Premises used: CategoryTheory.Limits.PullbackCone.mk, CategoryTheory.Limits.PullbackCone.equalizer_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
⊢ a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂

Tactic:
apply reassoc_of% comm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
⊢ m ≫ PullbackCone.fst (PullbackCone.mk a b ⋯) =
    (IsPullback.isLimit big_k).lift s' ≫ PullbackCone.fst (PullbackCone.mk a b ⋯)

Tactic:
apply m₁.trans (big_k.isLimit.fac s' WalkingCospan.left).symm

Premises used: CategoryTheory.Limits.WalkingCospan.left, Eq.symm, Eq.trans, CategoryTheory.Limits.IsLimit.fac, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
⊢ m ≫ PullbackCone.snd (PullbackCone.mk a b ⋯) =
    (IsPullback.isLimit big_k).lift s' ≫ PullbackCone.snd (PullbackCone.mk a b ⋯)

Tactic:
apply m₂.trans (big_k.isLimit.fac s' WalkingCospan.right).symm

Premises used: CategoryTheory.Limits.WalkingCospan.right, Eq.symm, Eq.trans, CategoryTheory.Limits.IsLimit.fac, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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₂
rw₃ rw₄ : b ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂
⊢ a ≫ f₁ = b ≫ f₁

Tactic:
rw [← cancel_mono f₂, assoc, assoc, big_k.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
rw rw₁ : b ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂
⊢ a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂

Tactic:
rw [small_k.w_assoc]

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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₂
rw₃ rw₄ : s.snd ≫ f₁ ≫ f₂ = s.snd ≫ f₁ ≫ f₂
⊢ s.fst ≫ f₁ = s.snd ≫ f₁

Tactic:
rw [← cancel_mono f₂, assoc, s.condition, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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₂)),
    (fun (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) ↦ small_k.lift s.fst s.snd ⋯) s ≫ (PullbackCone.mk a b ⋯).fst = s.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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₂)),
    (fun (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) ↦ small_k.lift s.fst s.snd ⋯) s ≫ (PullbackCone.mk a b ⋯).snd = s.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
refine :
  ∀ (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) (m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt),
    (∀ (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
⊢ IsLimit (PullbackCone.mk a b ⋯)

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) ?_

Premises used: CategoryTheory.Limits.PullbackCone.isLimitAux
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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 :
  ∀ (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
⊢ m = (fun (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) ↦ small_k.lift s.fst s.snd ⋯) s

Tactic:
apply small_k.isLimit.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
apply₁ :
  m ≫ (IsPullback.cone small_k).snd =
    (fun (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) ↦ small_k.lift s.fst s.snd ⋯) s ≫ (IsPullback.cone small_k).snd
⊢ ∀ (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

Tactic:
apply PullbackCone.equalizer_ext small_k.cone _ _

Premises used: CategoryTheory.Limits.PullbackCone.equalizer_ext, CategoryTheory.IsPullback.cone
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
⊢ s.π.app WalkingCospan.left =
    (fun (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) ↦ small_k.lift s.fst s.snd ⋯) s ≫ (IsPullback.cone small_k).fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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 ≫ (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

Tactic:
exact (hm WalkingCospan.left).trans (by simp)

Premises used: CategoryTheory.Limits.WalkingCospan.left, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
⊢ s.π.app WalkingCospan.right =
    (fun (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) ↦ small_k.lift s.fst s.snd ⋯) s ≫ (IsPullback.cone small_k).snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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 ≫ (IsPullback.cone small_k).snd =
    (fun (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) ↦ small_k.lift s.fst s.snd ⋯) s ≫ (IsPullback.cone small_k).snd

Tactic:
exact (hm WalkingCospan.right).trans (by simp)

Premises used: CategoryTheory.Limits.WalkingCospan.right, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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 ⋯)
⊢ t ≫ a = r.left

Tactic:
have ht : t ≫ a = r.left := k.isLimit.fac _ WalkingCospan.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
⊢ t ≫ b = r.right

Tactic:
have kt : t ≫ b = r.right := k.isLimit.fac _ WalkingCospan.right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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.π
rw₃ rw₄ : r.right ≫ s.π = r.right ≫ s.π
⊢ r.left ≫ s.π = r.right ≫ s.π

Tactic:
rw [← ht, assoc, s.condition, reassoc_of% kt]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cofork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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.π
refine_2 :
  ∀ (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
⊢ IsColimit (Cofork.ofπ f ⋯)

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 => ?_)

Premises used: CategoryTheory.Limits.Cofork.IsColimit.mk, CategoryTheory.RegularEpi.isColimit, CategoryTheory.Limits.Cofork.IsColimit.desc, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
⊢ (Cofork.ofπ f ⋯).π ≫ (fun (s : Cofork a b) ↦ Cofork.IsColimit.desc r.isColimit s.π ⋯) s = s.π

Tactic:
apply Cofork.IsColimit.π_desc' r.isColimit

Premises used: CategoryTheory.RegularEpi.isColimit, CategoryTheory.Limits.Cofork.IsColimit.π_desc'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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.π
refine_2 :
  (Cofork.ofπ f ⋯).π ≫ m = (Cofork.ofπ f ⋯).π ≫ (fun (s : Cofork a b) ↦ Cofork.IsColimit.desc r.isColimit s.π ⋯) s
⊢ m = (fun (s : Cofork a b) ↦ Cofork.IsColimit.desc r.isColimit s.π ⋯) s

Tactic:
apply Cofork.IsColimit.hom_ext r.isColimit

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext, CategoryTheory.RegularEpi.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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.π
⊢ (Cofork.ofπ f ⋯).π ≫ m = (Cofork.ofπ f ⋯).π ≫ (fun (s : Cofork a b) ↦ Cofork.IsColimit.desc r.isColimit s.π ⋯) s

Tactic:
w.trans (Cofork.IsColimit.π_desc' r.isColimit _ _).symm

Premises used: CategoryTheory.Limits.Cofork.ofπ, CategoryTheory.RegularEpi.isColimit, CategoryTheory.Limits.Cofork.IsColimit.π_desc', Eq.symm, Eq.trans, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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.π
⊢ (Cofork.ofπ f ⋯).π ≫ m = (Cofork.ofπ f ⋯).π ≫ (fun (s : Cofork a b) ↦ Cofork.IsColimit.desc r.isColimit s.π ⋯) s

Tactic:
exact w.trans (Cofork.IsColimit.π_desc' r.isColimit _ _).symm

Premises used: CategoryTheory.RegularEpi.isColimit, CategoryTheory.Limits.Cofork.IsColimit.π_desc', Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
R X_1 Y_1 Z_1 : C
f_1 : X_1 ⟶ Y_1
a b : R ⟶ X_1
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)
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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))
rw₁ rw₂ : Eq (α := pullback f (a₁ ≫ g) ⟶ X) (pullback.fst f (a₁ ≫ g) ≫ 𝟙 X) (pullback.fst f (a₁ ≫ g) ≫ 𝟙 X)
⊢ 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))

Tactic:
rw [pullback.lift_fst, pullback.lift_fst]

Premises used: CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
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

Tactic:
simp_rw [Category.assoc, ← pullback.condition, ← Category.assoc, s.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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.fst f g) ≫ f = h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯ ≫ a₁ ≫ g

Tactic:
simp only [assoc, lift_fst_assoc, pullback.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsKernelPair.lift_fst_assoc, CategoryTheory.Limits.pullback.condition