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 : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst_1 : Mono f
rw : IsIso ((IsPullback.isLimit ⋯).conePointUniqueUpToIso (IsPullback.isLimit h)).inv
⊢ IsIso a

Tactic:
rw [←
    show _ = a from
      (Category.comp_id _).symm.trans
        ((IsKernelPair.id_of_mono f).isLimit.conePointUniqueUpToIso_inv_comp h.isLimit
          WalkingCospan.left)]

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Category.comp_id, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.WalkingCospan.left, Eq.symm, CategoryTheory.IsKernelPair.id_of_mono, CategoryTheory.Iso.inv, Eq.trans, CategoryTheory.IsPullback.isLimit
-- 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
h : IsKernelPair f a b
inst_1 : Mono f
⊢ IsIso ((IsPullback.isLimit ⋯).conePointUniqueUpToIso (IsPullback.isLimit h)).inv

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst_1 : IsIso a
inst_2 : Mono f
⊢ IsPullback a (a ≫ 𝟙 X) (𝟙 X ≫ f) f

Tactic:
(IsPullback.of_horiz_isIso ⟨(rfl : a ≫ 𝟙 X = _)⟩).paste_vert (IsKernelPair.id_of_mono f)

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.IsPullback.paste_vert, CategoryTheory.IsKernelPair.id_of_mono, rfl, CategoryTheory.IsPullback.of_horiz_isIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst_1 : IsIso a
inst_2 : Mono f
h : a = a ≫ 𝟙 X
h₁ : f = 𝟙 X ≫ f
⊢ IsPullback a a f f

Tactic:
convert! (IsPullback.of_horiz_isIso ⟨(rfl : a ≫ 𝟙 X = _)⟩).paste_vert (IsKernelPair.id_of_mono f)

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.IsPullback.paste_vert, CategoryTheory.IsKernelPair.id_of_mono, rfl, CategoryTheory.IsPullback.of_horiz_isIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst_1 : IsIso a
inst_2 : Mono f
⊢ a = a ≫ 𝟙 X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst_1 : IsIso a
inst_2 : Mono f
⊢ a = a ≫ 𝟙 X

Tactic:
{ simp }
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst_1 : IsIso a
inst_2 : Mono f
⊢ f = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst_1 : IsIso a
inst_2 : Mono f
⊢ f = 𝟙 X ≫ f

Tactic:
{ simp }
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullback f f
⊢ IsKernelPair (R := pullback f f) f (pullback.fst f f) (pullback.snd f f)

Tactic:
IsPullback.of_hasPullback f f

Premises used: CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
π : X ⟶ Y
inst_1 : IsRegularEpi π
Z : C
fst snd : Z ⟶ X
h : IsKernelPair π fst snd
W : C
f : X ⟶ W
w : fst ≫ f = snd ≫ f
⊢ ∃ (g : Y ⟶ W), π ≫ g = f

Tactic:
⟨h.toCoequalizer'.desc (Cofork.ofπ f w), Cofork.IsColimit.π_desc h.toCoequalizer'⟩

Premises used: CategoryTheory.IsKernelPair.toCoequalizer', CategoryTheory.Limits.Cofork.ofπ, CategoryTheory.Limits.IsColimit.desc, Exists.intro, CategoryTheory.Limits.Cofork.IsColimit.π_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
s : KernelFork f
rw : Eq (α := s.pt ⟶ Y) (Fork.ι s ≫ 0) 0
rw₁ rw₂ : Eq.{v + 1} (α := s.pt ⟶ Y) 0 0
⊢ Fork.ι s ≫ f = 0

Tactic:
rw [Fork.condition, HasZeroMorphisms.comp_zero]

Premises used: CategoryTheory.Limits.Fork.condition, CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
s : KernelFork f
⊢ s.π.app one = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
ι : Z ⟶ X
w : ι ≫ f = 0
rw : Eq (α := Z ⟶ Y) 0 (ι ≫ 0)
rw₁ rw₂ : Eq.{v + 1} (α := Z ⟶ Y) 0 0
⊢ ι ≫ f = ι ≫ 0

Tactic:
rw [w, HasZeroMorphisms.comp_zero]

Premises used: CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y P : C
f : X ⟶ Y
ι : P ⟶ X
w : ι ≫ f = 0
⊢ Fork.ι (ofι ι w) = ι

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
s : Fork f 0
⊢ ∀ (j : WalkingParallelPair), s.π.app j = Iso.hom (Iso.refl s.pt) ≫ (Fork.ofι s.ι ⋯).π.app j

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
P : C
ι ι' : P ⟶ X
w : ι ≫ f = 0
h : ι = ι'
rw : ι ≫ f = 0
rw₁ rw₂ : Eq.{v + 1} (α := P ⟶ Y) 0 0
⊢ ι' ≫ f = 0

Tactic:
rw [← h, w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u'
inst_2 : Category.{v, u'} D
inst_3 : HasZeroMorphisms.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : F.IsEquivalence
app : (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
  fun (j : WalkingParallelPair) ↦
    match (motive := (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j) j with
    | zero => Iso.refl ((parallelPair f 0 ⋙ F).obj zero)
    | one => Iso.refl ((parallelPair f 0 ⋙ F).obj one)
⊢ (parallelPair f 0 ⋙ F).map (WalkingParallelPairHom.id zero) ≫ (app zero).hom =
    (app zero).hom ≫ (parallelPair (F.map f) 0).map (WalkingParallelPairHom.id zero)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u'
inst_2 : Category.{v, u'} D
inst_3 : HasZeroMorphisms.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : F.IsEquivalence
app : (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
  fun (j : WalkingParallelPair) ↦
    match (motive := (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j) j with
    | zero => Iso.refl ((parallelPair f 0 ⋙ F).obj zero)
    | one => Iso.refl ((parallelPair f 0 ⋙ F).obj one)
⊢ (parallelPair f 0 ⋙ F).map WalkingParallelPairHom.left ≫ (app one).hom =
    (app zero).hom ≫ (parallelPair (F.map f) 0).map WalkingParallelPairHom.left

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u'
inst_2 : Category.{v, u'} D
inst_3 : HasZeroMorphisms.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : F.IsEquivalence
app : (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
  fun (j : WalkingParallelPair) ↦
    match (motive := (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j) j with
    | zero => Iso.refl ((parallelPair f 0 ⋙ F).obj zero)
    | one => Iso.refl ((parallelPair f 0 ⋙ F).obj one)
⊢ (parallelPair f 0 ⋙ F).map WalkingParallelPairHom.right ≫ (app one).hom =
    (app zero).hom ≫ (parallelPair (F.map f) 0).map WalkingParallelPairHom.right

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u'
inst_2 : Category.{v, u'} D
inst_3 : HasZeroMorphisms.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : F.IsEquivalence
app : (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
  fun (j : WalkingParallelPair) ↦
    match (motive := (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j) j with
    | zero => Iso.refl ((parallelPair f 0 ⋙ F).obj zero)
    | one => Iso.refl ((parallelPair f 0 ⋙ F).obj one)
⊢ (parallelPair f 0 ⋙ F).map (WalkingParallelPairHom.id one) ≫ (app one).hom =
    (app one).hom ≫ (parallelPair (F.map f) 0).map (WalkingParallelPairHom.id one)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
t : KernelFork f
lift : (s : KernelFork f) → s.pt ⟶ t.pt
fac : ∀ (s : KernelFork f), lift s ≫ Fork.ι t = Fork.ι s
uniq : ∀ (s : KernelFork f) (m : s.pt ⟶ t.pt), m ≫ Fork.ι t = Fork.ι s → m = lift s
s : Cone (parallelPair f 0)
j : WalkingParallelPair
zero : lift s ≫ t.π.app WalkingParallelPair.zero = s.π.app WalkingParallelPair.zero
one : lift s ≫ t.π.app WalkingParallelPair.one = s.π.app WalkingParallelPair.one
⊢ lift s ≫ t.π.app j = s.π.app j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
t : KernelFork f
lift : (s : KernelFork f) → s.pt ⟶ t.pt
fac : ∀ (s : KernelFork f), lift s ≫ Fork.ι t = Fork.ι s
uniq : ∀ (s : KernelFork f) (m : s.pt ⟶ t.pt), m ≫ Fork.ι t = Fork.ι s → m = lift s
s : Cone (parallelPair f 0)
⊢ lift s ≫ t.π.app zero = s.π.app zero

Tactic:
fac s

Premises used: CategoryTheory.Limits.Fork.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
t : KernelFork f
lift : (s : KernelFork f) → s.pt ⟶ t.pt
fac : ∀ (s : KernelFork f), lift s ≫ Fork.ι t = Fork.ι s
uniq : ∀ (s : KernelFork f) (m : s.pt ⟶ t.pt), m ≫ Fork.ι t = Fork.ι s → m = lift s
s : Cone (parallelPair f 0)
⊢ lift s ≫ t.π.app zero = s.π.app zero

Tactic:
exact fac s
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
t : KernelFork f
lift : (s : KernelFork f) → s.pt ⟶ t.pt
fac : ∀ (s : KernelFork f), lift s ≫ Fork.ι t = Fork.ι s
uniq : ∀ (s : KernelFork f) (m : s.pt ⟶ t.pt), m ≫ Fork.ι t = Fork.ι s → m = lift s
s : Cone (parallelPair f 0)
⊢ lift s ≫ t.π.app one = s.π.app one

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y K : C
f : X ⟶ Y
i : K ⟶ X
w : i ≫ f = 0
h : {A : C} → (k : A ⟶ X) → k ≫ f = 0 → { l : A ⟶ K // l ≫ i = k }
hi : Mono i
A : C
k : A ⟶ X
hk : k ≫ f = 0
m : A ⟶ K
hm : m ≫ i = k
rw : m ≫ i = (fun {x : C} (k : x ⟶ X) (hk : k ≫ f = 0) ↦ (↑(h k hk) : x ⟶ K)) k hk ≫ i
rw₁ : m ≫ i = k
rw₂ rw₃ : k = k
⊢ m = (fun {x : C} (k : x ⟶ X) (hk : k ≫ f = 0) ↦ (↑(h k hk) : x ⟶ K)) k hk

Tactic:
rw [← cancel_mono i, (h k hk).2, hm]

Premises used: CategoryTheory.cancel_mono, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
⊢ Fork.ι c ≫ h = 0

Tactic:
simp [hh]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
rw : (s.ι ≫ f) ≫ g = (s.ι ≫ 0) ≫ g
⊢ s.ι ≫ f = s.ι ≫ 0

Tactic:
rw [← cancel_mono g]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
⊢ (s.ι ≫ f) ≫ g = (s.ι ≫ 0) ≫ g

Tactic:
simp [← hh, s.condition]

Premises used: CategoryTheory.Limits.Fork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m ≫ Fork.ι (KernelFork.ofι (Fork.ι c) ⋯) = s.ι
apply : m ≫ Fork.ι c = (↑l : s'.pt ⟶ c.pt) ≫ Fork.ι c
⊢ m = (↑l : s'.pt ⟶ c.pt)

Tactic:
apply Fork.IsLimit.hom_ext i

Premises used: CategoryTheory.Limits.Fork.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m ≫ Fork.ι (KernelFork.ofι (Fork.ι c) ⋯) = s.ι
⊢ m ≫ Fork.ι c = s.ι

Tactic:
rw [Fork.ι_ofι] at hm

Premises used: CategoryTheory.Limits.Fork.ι_ofι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m ≫ Fork.ι c = s.ι
rw : s.ι = (↑l : s'.pt ⟶ c.pt) ≫ Fork.ι c
⊢ m ≫ Fork.ι c = (↑l : s'.pt ⟶ c.pt) ≫ Fork.ι c

Tactic:
rw [hm]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m ≫ Fork.ι c = s.ι
⊢ s.ι = (↑l : s'.pt ⟶ c.pt) ≫ Fork.ι c

Tactic:
l.2.symm

Premises used: CategoryTheory.Limits.Fork.ofι, CategoryTheory.Limits.Fork.ι, Eq.symm, CategoryTheory.Limits.parallelPair, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m ≫ Fork.ι c = s.ι
⊢ s.ι = (↑l : s'.pt ⟶ c.pt) ≫ Fork.ι c

Tactic:
exact l.2.symm

Premises used: Eq.symm, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : KernelFork h
rw : Fork.ι s ≫ h = (Fork.ι s ≫ 0) ≫ g
⊢ Fork.ι s ≫ f = Fork.ι s ≫ 0

Tactic:
rw [← cancel_mono g, Category.assoc, ← hh]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : KernelFork h
⊢ Fork.ι s ≫ h = (Fork.ι s ≫ 0) ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : KernelFork h
⊢ (isKernelCompMono i g hh).lift s = i.lift (Fork.ofι (Fork.ι s) ⋯)

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ofι, CategoryTheory.Limits.Fork.ι, CategoryTheory.Limits.parallelPair, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
W : C
g : Y ⟶ W
h : X ⟶ W
c : KernelFork h
i : IsLimit c
hf : Fork.ι c ≫ f = 0
hfg : f ≫ g = h
s : Fork f 0
⊢ s.ι ≫ h = 0

Tactic:
simp [← hfg]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
W : C
g : Y ⟶ W
h : X ⟶ W
c : KernelFork h
i : IsLimit c
hf : Fork.ι c ≫ f = 0
hfg : f ≫ g = h
s : Fork f 0
⊢ (fun (s : Fork f 0) ↦ (i.lift (KernelFork.ofι s.ι ⋯) : (KernelFork.ofι s.ι ⋯).pt ⟶ c.pt)) s ≫
      Fork.ι (KernelFork.ofι (Fork.ι c) hf) =
    s.ι

Tactic:
simp only [KernelFork.ι_ofι, Fork.IsLimit.lift_ι]

Premises used: CategoryTheory.Limits.KernelFork.ι_ofι, CategoryTheory.Limits.Fork.IsLimit.lift_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
W : C
g : Y ⟶ W
h_1 : X ⟶ W
c : KernelFork h_1
i : IsLimit c
hf : Fork.ι c ≫ f = 0
hfg : f ≫ g = h_1
s : Fork f 0
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) hf).pt
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι c) hf) = s.ι
apply :
  m ≫ Fork.ι c = (fun (s : Fork f 0) ↦ (i.lift (KernelFork.ofι s.ι ⋯) : (KernelFork.ofι s.ι ⋯).pt ⟶ c.pt)) s ≫ Fork.ι c
⊢ m = (fun (s : Fork f 0) ↦ (i.lift (KernelFork.ofι s.ι ⋯) : (KernelFork.ofι s.ι ⋯).pt ⟶ c.pt)) s

Tactic:
apply Fork.IsLimit.hom_ext i

Premises used: CategoryTheory.Limits.Fork.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
W : C
g : Y ⟶ W
h_1 : X ⟶ W
c : KernelFork h_1
i : IsLimit c
hf : Fork.ι c ≫ f = 0
hfg : f ≫ g = h_1
s : Fork f 0
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) hf).pt
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι c) hf) = s.ι
⊢ m ≫ Fork.ι c = (fun (s : Fork f 0) ↦ (i.lift (KernelFork.ofι s.ι ⋯) : (KernelFork.ofι s.ι ⋯).pt ⟶ c.pt)) s ≫ Fork.ι c

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y : C
f : X ⟶ Y
hf : f = 0
rw : Eq.{v + 1} (α := X ⟶ Y) (𝟙 X ≫ 0) 0
rw₁ rw₂ : Eq.{v + 1} (α := X ⟶ Y) 0 0
⊢ 𝟙 X ≫ f = 0

Tactic:
rw [hf, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y : C
f : X ⟶ Y
hf : f = 0
W' : C
x : W' ⟶ X
h : x ≫ f = 0
x_1 : W' ⟶ X
hb : x_1 ≫ 𝟙 X = x
⊢ x_1 = (fun {W' : C} (x : W' ⟶ X) (x_2 : x ≫ f = 0) ↦ x) x h

Tactic:
simp only [← hb, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y : C
f : X ⟶ Y
c : KernelFork f
hf : Mono f
h : IsZero.{v, u} c.pt
s : KernelFork f
rw : 0 = Fork.ι s
rw₁ : 0 ≫ f = Fork.ι s ≫ f
rw₂ : 0 = Fork.ι s ≫ f
rw₃ rw₄ : Eq.{v + 1} (α := s.pt ⟶ Y) 0 0
⊢ (fun (x : KernelFork f) ↦ (0 : x.pt ⟶ c.pt)) s ≫ Fork.ι c = Fork.ι s

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

Premises used: CategoryTheory.Limits.KernelFork.condition, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
hf : f = 0
⊢ IsIso (Fork.ι c)

Tactic:
isIso_limit_cone_parallelPair_of_eq hf hc

Premises used: CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
X' Y' : C
g' : X' ⟶ Y'
e : X ≅ X'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0
⊢ (Fork.ι c ≫ e.hom) ≫ g' = 0

Tactic:
simp [← iff]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
X' Y' : C
g' : X' ⟶ Y'
e : X ≅ X'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0
W' : C
s : W' ⟶ X'
hs : s ≫ g' = 0
rw : (s ≫ e.inv) ≫ e.hom ≫ g' = 0
rw₁ : s ≫ e.inv ≫ e.hom ≫ g' = 0
rw₂ : s ≫ g' = 0
rw₃ rw₄ : Eq.{v + 1} (α := W' ⟶ Y') 0 0
⊢ (s ≫ e.inv) ≫ g = 0

Tactic:
rw [iff, Category.assoc, Iso.inv_hom_id_assoc, hs]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
X' Y' : C
g' : X' ⟶ Y'
e : X ≅ X'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0
W' : C
s : W' ⟶ X'
hs : s ≫ g' = 0
⊢ (fun {W' : C} (s : W' ⟶ X') (hs : s ≫ g' = 0) ↦ (hc.lift (ofι (s ≫ e.inv) ⋯) : (ofι (s ≫ e.inv) ⋯).pt ⟶ c.pt)) s hs ≫
      Fork.ι c ≫ e.hom =
    s

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
X' Y' : C
g' : X' ⟶ Y'
e : X ≅ X'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0
W' : C
s : W' ⟶ X'
hs : s ≫ g' = 0
m : W' ⟶ c.pt
hm : m ≫ Fork.ι c ≫ e.hom = s
⊢ m ≫ Fork.ι c =
    (fun {W' : C} (s : W' ⟶ X') (hs : s ≫ g' = 0) ↦ (hc.lift (ofι (s ≫ e.inv) ⋯) : (ofι (s ≫ e.inv) ⋯).pt ⟶ c.pt)) s
        hs ≫
      Fork.ι c

Tactic:
simpa [← cancel_mono e.hom] using hm

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
Y' : C
g' : X ⟶ Y'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ g' = 0
⊢ Fork.ι c ≫ g' = 0

Tactic:
simp [← iff]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
Y' : C
g' : X ⟶ Y'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ g' = 0
⊢ ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ Iso.hom (Iso.refl X) ≫ g' = 0

Tactic:
simpa using iff
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
inst_2 : Mono f
⊢ Mono (Fork.ι c)

Tactic:
have := Fork.IsLimit.mono hc