no goals
C : Type u
inst✝¹ : Category 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₂
rw [small_k.w_assoc]
C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app j) →
      m =
        (fun s =>
            lift small_k (PullbackCone.fst s) (PullbackCone.snd s)
              (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
          s
C : Type u
inst✝¹ : Category 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₂))
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) _
no goals
C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app j) →
      m =
        (fun s =>
            lift small_k (PullbackCone.fst s) (PullbackCone.snd s)
              (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
          s
. intro s m hm
  apply small_k.isLimit.hom_ext
  apply PullbackCone.equalizer_ext small_k.cone _ _
  . exact (hm WalkingCospan.left).trans (by simp)
  . exact (hm WalkingCospan.right).trans (by simp)
no goals
C : Type u
inst✝¹ : Category 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₁
rw [← cancel_mono f₂, assoc, s.condition, assoc]
no goals
C : Type u
inst✝¹ : Category 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
simp
no goals
C : Type u
inst✝¹ : Category 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
simp
C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app j
⊢ m =
    (fun s =>
        lift small_k (PullbackCone.fst s) (PullbackCone.snd s) (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
      s
C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app j) →
      m =
        (fun s =>
            lift small_k (PullbackCone.fst s) (PullbackCone.snd s)
              (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
          s
intro s m hm
C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app j
⊢ ∀ (j : WalkingCospan),
    m ≫ (IsPullback.cone small_k).π.app j =
      (fun s =>
            lift small_k (PullbackCone.fst s) (PullbackCone.snd s)
              (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
          s ≫
        (IsPullback.cone small_k).π.app j
C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app j
⊢ m =
    (fun s =>
        lift small_k (PullbackCone.fst s) (PullbackCone.snd s) (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
      s
apply small_k.isLimit.hom_ext
C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app 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)

C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app 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)
C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app j
⊢ ∀ (j : WalkingCospan),
    m ≫ (IsPullback.cone small_k).π.app j =
      (fun s =>
            lift small_k (PullbackCone.fst s) (PullbackCone.snd s)
              (_ : PullbackCone.fst s ≫ f₁ = PullbackCone.snd s ≫ f₁))
          s ≫
        (IsPullback.cone small_k).π.app j
apply PullbackCone.equalizer_ext small_k.cone _ _
C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app 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)
C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app 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)

C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app 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)
. exact (hm WalkingCospan.left).trans (by simp)
no goals
C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app 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)
. exact (hm WalkingCospan.right).trans (by simp)
no goals
C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app 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)
exact (hm WalkingCospan.left).trans (by simp)
no goals
C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app j
⊢ s.π.app 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)
simp
no goals
C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app 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)
exact (hm WalkingCospan.right).trans (by simp)
no goals
C : Type u
inst✝¹ : Category 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 ≫ (PullbackCone.mk a b (_ : a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂)).π.app j = s.π.app j
⊢ s.π.app 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)
simp