[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
[PROOFSTEP]
cases P
[GOAL]
case mk
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
Q : IsKernelPair f a b
toCommSq✝ : CommSq a b f f
isLimit'✝ : Nonempty (IsLimit (PullbackCone.mk a b (_ : a ≫ f = b ≫ f)))
⊢ (_ : IsPullback a b f f) = Q
[PROOFSTEP]
cases Q
[GOAL]
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
toCommSq✝¹ : CommSq a b f f
isLimit'✝¹ : Nonempty (IsLimit (PullbackCone.mk a b (_ : a ≫ f = b ≫ f)))
toCommSq✝ : CommSq a b f f
isLimit'✝ : Nonempty (IsLimit (PullbackCone.mk a b (_ : a ≫ f = b ≫ f)))
⊢ (_ : IsPullback a b f f) = (_ : IsPullback a b f f)
[PROOFSTEP]
congr
[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
⊢ lift k p q w ≫ a = p ∧ lift k p q w ≫ b = q
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
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₁
⊢ { l //
    l ≫ PullbackCone.fst (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.fst s ∧
      l ≫ PullbackCone.snd (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.snd s ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)).pt},
          m ≫ PullbackCone.fst (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.fst s →
            m ≫ PullbackCone.snd (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.snd s → m = l }
[PROOFSTEP]
let s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd (s.condition_assoc _)
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
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 (PullbackCone.fst s) (PullbackCone.snd s)
    (_ : PullbackCone.fst s ≫ f₁ ≫ f₂ = PullbackCone.snd s ≫ f₁ ≫ f₂)
⊢ { l //
    l ≫ PullbackCone.fst (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.fst s ∧
      l ≫ PullbackCone.snd (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.snd s ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)).pt},
          m ≫ PullbackCone.fst (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.fst s →
            m ≫ PullbackCone.snd (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.snd s → m = l }
[PROOFSTEP]
refine'
  ⟨big_k.isLimit.lift s', big_k.isLimit.fac _ WalkingCospan.left, big_k.isLimit.fac _ WalkingCospan.right, fun m₁ m₂ =>
    _⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
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 (PullbackCone.fst s) (PullbackCone.snd s)
    (_ : PullbackCone.fst s ≫ f₁ ≫ f₂ = PullbackCone.snd s ≫ f₁ ≫ f₂)
m✝ : s.pt ⟶ (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)).pt
m₁ : m✝ ≫ PullbackCone.fst (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.fst s
m₂ : m✝ ≫ PullbackCone.snd (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.snd s
⊢ m✝ = IsLimit.lift (IsPullback.isLimit big_k) s'
[PROOFSTEP]
apply big_k.isLimit.hom_ext
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
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 (PullbackCone.fst s) (PullbackCone.snd s)
    (_ : PullbackCone.fst s ≫ f₁ ≫ f₂ = PullbackCone.snd s ≫ f₁ ≫ f₂)
m✝ : s.pt ⟶ (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)).pt
m₁ : m✝ ≫ PullbackCone.fst (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.fst s
m₂ : m✝ ≫ PullbackCone.snd (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.snd s
⊢ ∀ (j : WalkingCospan),
    m✝ ≫ NatTrans.app (IsPullback.cone big_k).π j =
      IsLimit.lift (IsPullback.isLimit big_k) s' ≫ NatTrans.app (IsPullback.cone big_k).π j
[PROOFSTEP]
refine' (PullbackCone.mk a b _ : PullbackCone (f₁ ≫ f₂) _).equalizer_ext _ _
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
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 (PullbackCone.fst s) (PullbackCone.snd s)
    (_ : PullbackCone.fst s ≫ f₁ ≫ f₂ = PullbackCone.snd s ≫ f₁ ≫ f₂)
m✝ : s.pt ⟶ (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)).pt
m₁ : m✝ ≫ PullbackCone.fst (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.fst s
m₂ : m✝ ≫ PullbackCone.snd (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.snd s
⊢ a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂
[PROOFSTEP]
apply reassoc_of% comm
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
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 (PullbackCone.fst s) (PullbackCone.snd s)
    (_ : PullbackCone.fst s ≫ f₁ ≫ f₂ = PullbackCone.snd s ≫ f₁ ≫ f₂)
m✝ : s.pt ⟶ (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)).pt
m₁ : m✝ ≫ PullbackCone.fst (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.fst s
m₂ : m✝ ≫ PullbackCone.snd (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.snd s
⊢ m✝ ≫ PullbackCone.fst (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)) =
    IsLimit.lift (IsPullback.isLimit big_k) s' ≫ PullbackCone.fst (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂))
[PROOFSTEP]
apply m₁.trans (big_k.isLimit.fac s' WalkingCospan.left).symm
[GOAL]
case refine'_3
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
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 (PullbackCone.fst s) (PullbackCone.snd s)
    (_ : PullbackCone.fst s ≫ f₁ ≫ f₂ = PullbackCone.snd s ≫ f₁ ≫ f₂)
m✝ : s.pt ⟶ (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)).pt
m₁ : m✝ ≫ PullbackCone.fst (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.fst s
m₂ : m✝ ≫ PullbackCone.snd (PullbackCone.mk a b (_ : a ≫ f₁ = b ≫ f₁)) = PullbackCone.snd s
⊢ m✝ ≫ PullbackCone.snd (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)) =
    IsLimit.lift (IsPullback.isLimit big_k) s' ≫ PullbackCone.snd (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂))
[PROOFSTEP]
apply m₂.trans (big_k.isLimit.fac s' WalkingCospan.right).symm
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
big_k : IsKernelPair (f₁ ≫ f₂) a b
⊢ a ≫ f₁ = b ≫ f₁
[PROOFSTEP]
rw [← cancel_mono f₂, assoc, assoc, big_k.w]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
⊢ a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂
[PROOFSTEP]
rw [small_k.w_assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
⊢ IsLimit (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂))
[PROOFSTEP]
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) _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
⊢ PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁
[PROOFSTEP]
rw [← cancel_mono f₂, assoc, s.condition, assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
⊢ ∀ (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)),
    (fun s =>
            lift small_k (PullbackCone.fst s) (PullbackCone.snd s)
              (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
          s ≫
        PullbackCone.fst (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)) =
      PullbackCone.fst s
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
⊢ ∀ (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)),
    (fun s =>
            lift small_k (PullbackCone.fst s) (PullbackCone.snd s)
              (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
          s ≫
        PullbackCone.snd (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)) =
      PullbackCone.snd s
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
⊢ ∀ (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) (m : s.pt ⟶ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).pt),
    (∀ (j : WalkingCospan),
        m ≫ NatTrans.app (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π j = NatTrans.app s.π j) →
      m =
        (fun s =>
            lift small_k (PullbackCone.fst s) (PullbackCone.snd s)
              (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
          s
[PROOFSTEP]
intro s m hm
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).pt
hm :
  ∀ (j : WalkingCospan), m ≫ NatTrans.app (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π j = NatTrans.app s.π j
⊢ m =
    (fun s =>
        lift small_k (PullbackCone.fst s) (PullbackCone.snd s) (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
      s
[PROOFSTEP]
apply small_k.isLimit.hom_ext
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).pt
hm :
  ∀ (j : WalkingCospan), m ≫ NatTrans.app (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π j = NatTrans.app s.π j
⊢ ∀ (j : WalkingCospan),
    m ≫ NatTrans.app (IsPullback.cone small_k).π j =
      (fun s =>
            lift small_k (PullbackCone.fst s) (PullbackCone.snd s)
              (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
          s ≫
        NatTrans.app (IsPullback.cone small_k).π j
[PROOFSTEP]
apply PullbackCone.equalizer_ext small_k.cone _ _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).pt
hm :
  ∀ (j : WalkingCospan), m ≫ NatTrans.app (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π j = NatTrans.app s.π j
⊢ m ≫ PullbackCone.fst (IsPullback.cone small_k) =
    (fun s =>
          lift small_k (PullbackCone.fst s) (PullbackCone.snd s)
            (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
        s ≫
      PullbackCone.fst (IsPullback.cone small_k)
[PROOFSTEP]
exact (hm WalkingCospan.left).trans (by simp)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).pt
hm :
  ∀ (j : WalkingCospan), m ≫ NatTrans.app (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π j = NatTrans.app s.π j
⊢ NatTrans.app s.π WalkingCospan.left =
    (fun s =>
          lift small_k (PullbackCone.fst s) (PullbackCone.snd s)
            (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
        s ≫
      PullbackCone.fst (IsPullback.cone small_k)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).pt
hm :
  ∀ (j : WalkingCospan), m ≫ NatTrans.app (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π j = NatTrans.app s.π j
⊢ m ≫ PullbackCone.snd (IsPullback.cone small_k) =
    (fun s =>
          lift small_k (PullbackCone.fst s) (PullbackCone.snd s)
            (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
        s ≫
      PullbackCone.snd (IsPullback.cone small_k)
[PROOFSTEP]
exact (hm WalkingCospan.right).trans (by simp)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).pt
hm :
  ∀ (j : WalkingCospan), m ≫ NatTrans.app (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π j = NatTrans.app s.π j
⊢ NatTrans.app s.π WalkingCospan.right =
    (fun s =>
          lift small_k (PullbackCone.fst s) (PullbackCone.snd s)
            (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
        s ≫
      PullbackCone.snd (IsPullback.cone small_k)
[PROOFSTEP]
simp
[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
⊢ IsColimit (Cofork.ofπ f (_ : a ≫ f = b ≫ f))
[PROOFSTEP]
let t := k.isLimit.lift (PullbackCone.mk _ _ r.w)
[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 RegularEpi.left RegularEpi.right (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f)).pt ⟶
  (IsPullback.cone k).pt :=
  IsLimit.lift (IsPullback.isLimit k)
    (PullbackCone.mk RegularEpi.left RegularEpi.right (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f))
⊢ IsColimit (Cofork.ofπ f (_ : a ≫ f = b ≫ f))
[PROOFSTEP]
have ht : t ≫ a = r.left := k.isLimit.fac _ WalkingCospan.left
[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 RegularEpi.left RegularEpi.right (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f)).pt ⟶
  (IsPullback.cone k).pt :=
  IsLimit.lift (IsPullback.isLimit k)
    (PullbackCone.mk RegularEpi.left RegularEpi.right (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f))
ht : t ≫ a = RegularEpi.left
⊢ IsColimit (Cofork.ofπ f (_ : a ≫ f = b ≫ f))
[PROOFSTEP]
have kt : t ≫ b = r.right := k.isLimit.fac _ WalkingCospan.right
[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 RegularEpi.left RegularEpi.right (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f)).pt ⟶
  (IsPullback.cone k).pt :=
  IsLimit.lift (IsPullback.isLimit k)
    (PullbackCone.mk RegularEpi.left RegularEpi.right (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f))
ht : t ≫ a = RegularEpi.left
kt : t ≫ b = RegularEpi.right
⊢ IsColimit (Cofork.ofπ f (_ : a ≫ f = b ≫ f))
[PROOFSTEP]
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 => _)
[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 RegularEpi.left RegularEpi.right (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f)).pt ⟶
  (IsPullback.cone k).pt :=
  IsLimit.lift (IsPullback.isLimit k)
    (PullbackCone.mk RegularEpi.left RegularEpi.right (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f))
ht : t ≫ a = RegularEpi.left
kt : t ≫ b = RegularEpi.right
s : Cofork a b
⊢ RegularEpi.left ≫ Cofork.π s = RegularEpi.right ≫ Cofork.π s
[PROOFSTEP]
rw [← ht, assoc, s.condition, reassoc_of% kt]
[GOAL]
case refine'_1
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 RegularEpi.left RegularEpi.right (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f)).pt ⟶
  (IsPullback.cone k).pt :=
  IsLimit.lift (IsPullback.isLimit k)
    (PullbackCone.mk RegularEpi.left RegularEpi.right (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f))
ht : t ≫ a = RegularEpi.left
kt : t ≫ b = RegularEpi.right
s : Cofork a b
⊢ Cofork.π (Cofork.ofπ f (_ : a ≫ f = b ≫ f)) ≫
      (fun s =>
          Cofork.IsColimit.desc RegularEpi.isColimit (Cofork.π s)
            (_ : RegularEpi.left ≫ Cofork.π s = RegularEpi.right ≫ Cofork.π s))
        s =
    Cofork.π s
[PROOFSTEP]
apply Cofork.IsColimit.π_desc' r.isColimit
[GOAL]
case refine'_2
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 RegularEpi.left RegularEpi.right (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f)).pt ⟶
  (IsPullback.cone k).pt :=
  IsLimit.lift (IsPullback.isLimit k)
    (PullbackCone.mk RegularEpi.left RegularEpi.right (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f))
ht : t ≫ a = RegularEpi.left
kt : t ≫ b = RegularEpi.right
s : Cofork a b
m : (Cofork.ofπ f (_ : a ≫ f = b ≫ f)).pt ⟶ s.pt
w : Cofork.π (Cofork.ofπ f (_ : a ≫ f = b ≫ f)) ≫ m = Cofork.π s
⊢ m =
    (fun s =>
        Cofork.IsColimit.desc RegularEpi.isColimit (Cofork.π s)
          (_ : RegularEpi.left ≫ Cofork.π s = RegularEpi.right ≫ Cofork.π s))
      s
[PROOFSTEP]
apply Cofork.IsColimit.hom_ext r.isColimit
[GOAL]
case refine'_2
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 RegularEpi.left RegularEpi.right (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f)).pt ⟶
  (IsPullback.cone k).pt :=
  IsLimit.lift (IsPullback.isLimit k)
    (PullbackCone.mk RegularEpi.left RegularEpi.right (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f))
ht : t ≫ a = RegularEpi.left
kt : t ≫ b = RegularEpi.right
s : Cofork a b
m : (Cofork.ofπ f (_ : a ≫ f = b ≫ f)).pt ⟶ s.pt
w : Cofork.π (Cofork.ofπ f (_ : a ≫ f = b ≫ f)) ≫ m = Cofork.π s
⊢ Cofork.π (Cofork.ofπ f (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f)) ≫ m =
    Cofork.π (Cofork.ofπ f (_ : RegularEpi.left ≫ f = RegularEpi.right ≫ f)) ≫
      (fun s =>
          Cofork.IsColimit.desc RegularEpi.isColimit (Cofork.π s)
            (_ : RegularEpi.left ≫ Cofork.π s = RegularEpi.right ≫ Cofork.π s))
        s
[PROOFSTEP]
exact w.trans (Cofork.IsColimit.π_desc' r.isColimit _ _).symm
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
⊢ IsKernelPair pullback.fst
    (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
    (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
[PROOFSTEP]
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 hm => _)⟩⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
⊢ pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫ pullback.fst =
    pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫ pullback.fst
[PROOFSTEP]
rw [pullback.lift_fst, pullback.lift_fst]
[GOAL]
case refine'_1
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone pullback.fst pullback.fst
⊢ (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g
[PROOFSTEP]
simp_rw [Category.assoc, ← pullback.condition, ← Category.assoc, s.condition]
[GOAL]
case refine'_2
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone pullback.fst pullback.fst
⊢ (PullbackCone.fst s ≫ pullback.fst) ≫ f =
    lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
        (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g) ≫
      a₁ ≫ g
[PROOFSTEP]
simp only [assoc, lift_fst_assoc, pullback.condition]
[GOAL]
case refine'_3
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone pullback.fst pullback.fst
⊢ (fun s =>
          pullback.lift (PullbackCone.fst s ≫ pullback.fst)
            (lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
              (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g))
            (_ :
              (PullbackCone.fst s ≫ pullback.fst) ≫ f =
                lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                    (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g) ≫
                  a₁ ≫ g))
        s ≫
      PullbackCone.fst
        (PullbackCone.mk
          (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
          (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
          (_ :
            pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
                pullback.fst =
              pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
                pullback.fst)) =
    PullbackCone.fst s
[PROOFSTEP]
ext
[GOAL]
case refine'_3.h₀
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone pullback.fst pullback.fst
⊢ ((fun s =>
            pullback.lift (PullbackCone.fst s ≫ pullback.fst)
              (lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g))
              (_ :
                (PullbackCone.fst s ≫ pullback.fst) ≫ f =
                  lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                      (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g) ≫
                    a₁ ≫ g))
          s ≫
        PullbackCone.fst
          (PullbackCone.mk
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
            (_ :
              pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
                  pullback.fst =
                pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
                  pullback.fst))) ≫
      pullback.fst =
    PullbackCone.fst s ≫ pullback.fst
[PROOFSTEP]
simp
[GOAL]
case refine'_3.h₁
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone pullback.fst pullback.fst
⊢ ((fun s =>
            pullback.lift (PullbackCone.fst s ≫ pullback.fst)
              (lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g))
              (_ :
                (PullbackCone.fst s ≫ pullback.fst) ≫ f =
                  lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                      (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g) ≫
                    a₁ ≫ g))
          s ≫
        PullbackCone.fst
          (PullbackCone.mk
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
            (_ :
              pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
                  pullback.fst =
                pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
                  pullback.fst))) ≫
      pullback.snd =
    PullbackCone.fst s ≫ pullback.snd
[PROOFSTEP]
simp
[GOAL]
case refine'_4
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone pullback.fst pullback.fst
⊢ (fun s =>
          pullback.lift (PullbackCone.fst s ≫ pullback.fst)
            (lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
              (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g))
            (_ :
              (PullbackCone.fst s ≫ pullback.fst) ≫ f =
                lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                    (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g) ≫
                  a₁ ≫ g))
        s ≫
      PullbackCone.snd
        (PullbackCone.mk
          (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
          (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
          (_ :
            pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
                pullback.fst =
              pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
                pullback.fst)) =
    PullbackCone.snd s
[PROOFSTEP]
ext
[GOAL]
case refine'_4.h₀
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone pullback.fst pullback.fst
⊢ ((fun s =>
            pullback.lift (PullbackCone.fst s ≫ pullback.fst)
              (lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g))
              (_ :
                (PullbackCone.fst s ≫ pullback.fst) ≫ f =
                  lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                      (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g) ≫
                    a₁ ≫ g))
          s ≫
        PullbackCone.snd
          (PullbackCone.mk
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
            (_ :
              pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
                  pullback.fst =
                pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
                  pullback.fst))) ≫
      pullback.fst =
    PullbackCone.snd s ≫ pullback.fst
[PROOFSTEP]
simp [s.condition]
[GOAL]
case refine'_4.h₁
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone pullback.fst pullback.fst
⊢ ((fun s =>
            pullback.lift (PullbackCone.fst s ≫ pullback.fst)
              (lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g))
              (_ :
                (PullbackCone.fst s ≫ pullback.fst) ≫ f =
                  lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                      (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g) ≫
                    a₁ ≫ g))
          s ≫
        PullbackCone.snd
          (PullbackCone.mk
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
            (_ :
              pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
                  pullback.fst =
                pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
                  pullback.fst))) ≫
      pullback.snd =
    PullbackCone.snd s ≫ pullback.snd
[PROOFSTEP]
simp
[GOAL]
case refine'_5
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone pullback.fst pullback.fst
m :
  s.pt ⟶
    (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
        (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
        (_ :
          pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
              pullback.fst =
            pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
              pullback.fst)).pt
hm :
  ∀ (j : WalkingCospan),
    m ≫
        NatTrans.app
          (PullbackCone.mk
              (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
              (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
              (_ :
                pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
                    pullback.fst =
                  pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
                    pullback.fst)).π
          j =
      NatTrans.app s.π j
⊢ m =
    (fun s =>
        pullback.lift (PullbackCone.fst s ≫ pullback.fst)
          (lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
            (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g))
          (_ :
            (PullbackCone.fst s ≫ pullback.fst) ≫ f =
              lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                  (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g) ≫
                a₁ ≫ g))
      s
[PROOFSTEP]
apply pullback.hom_ext
[GOAL]
case refine'_5.h₀
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone pullback.fst pullback.fst
m :
  s.pt ⟶
    (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
        (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
        (_ :
          pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
              pullback.fst =
            pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
              pullback.fst)).pt
hm :
  ∀ (j : WalkingCospan),
    m ≫
        NatTrans.app
          (PullbackCone.mk
              (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
              (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
              (_ :
                pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
                    pullback.fst =
                  pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
                    pullback.fst)).π
          j =
      NatTrans.app s.π j
⊢ m ≫ pullback.fst =
    (fun s =>
          pullback.lift (PullbackCone.fst s ≫ pullback.fst)
            (lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
              (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g))
            (_ :
              (PullbackCone.fst s ≫ pullback.fst) ≫ f =
                lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                    (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g) ≫
                  a₁ ≫ g))
        s ≫
      pullback.fst
[PROOFSTEP]
simpa using hm WalkingCospan.left =≫ pullback.fst
[GOAL]
case refine'_5.h₁
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone pullback.fst pullback.fst
m :
  s.pt ⟶
    (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
        (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
        (_ :
          pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
              pullback.fst =
            pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
              pullback.fst)).pt
hm :
  ∀ (j : WalkingCospan),
    m ≫
        NatTrans.app
          (PullbackCone.mk
              (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
              (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
              (_ :
                pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
                    pullback.fst =
                  pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
                    pullback.fst)).π
          j =
      NatTrans.app s.π j
⊢ m ≫ pullback.snd =
    (fun s =>
          pullback.lift (PullbackCone.fst s ≫ pullback.fst)
            (lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
              (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g))
            (_ :
              (PullbackCone.fst s ≫ pullback.fst) ≫ f =
                lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                    (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g) ≫
                  a₁ ≫ g))
        s ≫
      pullback.snd
[PROOFSTEP]
apply PullbackCone.IsLimit.hom_ext h.isLimit
[GOAL]
case refine'_5.h₁.h₀
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone pullback.fst pullback.fst
m :
  s.pt ⟶
    (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
        (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
        (_ :
          pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
              pullback.fst =
            pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
              pullback.fst)).pt
hm :
  ∀ (j : WalkingCospan),
    m ≫
        NatTrans.app
          (PullbackCone.mk
              (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
              (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
              (_ :
                pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
                    pullback.fst =
                  pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
                    pullback.fst)).π
          j =
      NatTrans.app s.π j
⊢ (m ≫ pullback.snd) ≫ PullbackCone.fst (IsPullback.cone h) =
    ((fun s =>
            pullback.lift (PullbackCone.fst s ≫ pullback.fst)
              (lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g))
              (_ :
                (PullbackCone.fst s ≫ pullback.fst) ≫ f =
                  lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                      (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g) ≫
                    a₁ ≫ g))
          s ≫
        pullback.snd) ≫
      PullbackCone.fst (IsPullback.cone h)
[PROOFSTEP]
simpa using hm WalkingCospan.left =≫ pullback.snd
[GOAL]
case refine'_5.h₁.h₁
C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone pullback.fst pullback.fst
m :
  s.pt ⟶
    (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
        (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
        (_ :
          pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
              pullback.fst =
            pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
              pullback.fst)).pt
hm :
  ∀ (j : WalkingCospan),
    m ≫
        NatTrans.app
          (PullbackCone.mk
              (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g))
              (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g))
              (_ :
                pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₁ ≫ g) ≫
                    pullback.fst =
                  pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) (_ : f ≫ 𝟙 Z = 𝟙 X ≫ f) (_ : (a₁ ≫ g) ≫ 𝟙 Z = a₂ ≫ g) ≫
                    pullback.fst)).π
          j =
      NatTrans.app s.π j
⊢ (m ≫ pullback.snd) ≫ PullbackCone.snd (IsPullback.cone h) =
    ((fun s =>
            pullback.lift (PullbackCone.fst s ≫ pullback.fst)
              (lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g))
              (_ :
                (PullbackCone.fst s ≫ pullback.fst) ≫ f =
                  lift h (PullbackCone.fst s ≫ pullback.snd) (PullbackCone.snd s ≫ pullback.snd)
                      (_ : (PullbackCone.fst s ≫ pullback.snd) ≫ g = (PullbackCone.snd s ≫ pullback.snd) ≫ g) ≫
                    a₁ ≫ g))
          s ≫
        pullback.snd) ≫
      PullbackCone.snd (IsPullback.cone h)
[PROOFSTEP]
simpa using hm WalkingCospan.right =≫ pullback.snd
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
⊢ Mono f
[PROOFSTEP]
obtain ⟨l, h₁, h₂⟩ := Limits.PullbackCone.IsLimit.lift' h.isLimit (𝟙 _) (𝟙 _) (by simp [h.w])
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f
[PROOFSTEP]
simp [h.w]
[GOAL]
case mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l ≫ PullbackCone.fst (IsPullback.cone h) = 𝟙 X
h₂ : l ≫ PullbackCone.snd (IsPullback.cone h) = 𝟙 X
⊢ Mono f
[PROOFSTEP]
rw [IsPullback.cone_fst, ← IsIso.eq_comp_inv, Category.id_comp] at h₁
[GOAL]
case mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : l ≫ PullbackCone.snd (IsPullback.cone h) = 𝟙 X
⊢ Mono f
[PROOFSTEP]
rw [h₁, IsIso.inv_comp_eq, Category.comp_id] at h₂
[GOAL]
case mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : PullbackCone.snd (IsPullback.cone h) = a
⊢ Mono f
[PROOFSTEP]
constructor
[GOAL]
case mk.intro.right_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : PullbackCone.snd (IsPullback.cone h) = a
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
[PROOFSTEP]
intro Z g₁ g₂ e
[GOAL]
case mk.intro.right_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z✝ : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : PullbackCone.snd (IsPullback.cone h) = a
Z : C
g₁ g₂ : Z ⟶ X
e : g₁ ≫ f = g₂ ≫ f
⊢ g₁ = g₂
[PROOFSTEP]
obtain ⟨l', rfl, rfl⟩ := Limits.PullbackCone.IsLimit.lift' h.isLimit _ _ e
[GOAL]
case mk.intro.right_cancellation.mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z✝ : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : PullbackCone.snd (IsPullback.cone h) = a
Z : C
l' : Z ⟶ (IsPullback.cone h).pt
e : (l' ≫ PullbackCone.fst (IsPullback.cone h)) ≫ f = (l' ≫ PullbackCone.snd (IsPullback.cone h)) ≫ f
⊢ l' ≫ PullbackCone.fst (IsPullback.cone h) = l' ≫ PullbackCone.snd (IsPullback.cone h)
[PROOFSTEP]
rw [IsPullback.cone_fst, h₂]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : Mono f
⊢ IsIso a
[PROOFSTEP]
rw [←
  show _ = a from
    (Category.comp_id _).symm.trans
      ((IsKernelPair.id_of_mono f).isLimit.conePointUniqueUpToIso_inv_comp h.isLimit WalkingCospan.left)]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : Mono f
⊢ IsIso
    (IsLimit.conePointUniqueUpToIso (IsPullback.isLimit (_ : IsKernelPair f (𝟙 X) (𝟙 X))) (IsPullback.isLimit h)).inv
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ IsKernelPair f a a
[PROOFSTEP]
change IsPullback _ _ _ _
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ IsPullback a a f f
[PROOFSTEP]
convert (IsPullback.of_horiz_isIso ⟨(rfl : a ≫ 𝟙 X = _)⟩).paste_vert (IsKernelPair.id_of_mono f)
[GOAL]
case h.e'_8
C : Type u
inst✝² : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ a = a ≫ 𝟙 X
case h.e'_9
C : Type u
inst✝² : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ f = 𝟙 X ≫ f
[PROOFSTEP]
all_goals {simp
}
[GOAL]
case h.e'_8
C : Type u
inst✝² : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ a = a ≫ 𝟙 X
[PROOFSTEP]
{simp
}
[GOAL]
case h.e'_8
C : Type u
inst✝² : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ a = a ≫ 𝟙 X
[PROOFSTEP]
simp
[GOAL]
case h.e'_9
C : Type u
inst✝² : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ f = 𝟙 X ≫ f
[PROOFSTEP]
{simp
}
[GOAL]
case h.e'_9
C : Type u
inst✝² : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ f = 𝟙 X ≫ f
[PROOFSTEP]
simp