[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ IsIdempotentComplete C → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
[PROOFSTEP]
intro
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
[PROOFSTEP]
intro X p hp
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasEqualizer (𝟙 X) p
[PROOFSTEP]
rcases IsIdempotentComplete.idempotents_split X p hp with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
[GOAL]
case mp.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ HasEqualizer (𝟙 X) p
[PROOFSTEP]
exact
  ⟨Nonempty.intro
      { cone := Fork.ofι i (show i ≫ 𝟙 X = i ≫ p by rw [comp_id, ← h₂, ← assoc, h₁, id_comp])
        isLimit := by
          apply Fork.IsLimit.mk'
          intro s
          refine' ⟨s.ι ≫ e, _⟩
          constructor
          · erw [assoc, h₂, ← Limits.Fork.condition s, comp_id]
          · intro m hm
            rw [Fork.ι_ofι] at hm
            rw [← hm]
            simp only [← hm, assoc, h₁]
            exact (comp_id m).symm }⟩
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ i ≫ 𝟙 X = i ≫ p
[PROOFSTEP]
rw [comp_id, ← h₂, ← assoc, h₁, id_comp]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ IsLimit (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p))
[PROOFSTEP]
apply Fork.IsLimit.mk'
[GOAL]
case create
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ (s : Fork (𝟙 X) p) →
    { l //
      l ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s ∧
        ∀
          {m :
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
              ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj
                WalkingParallelPair.zero},
          m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = l }
[PROOFSTEP]
intro s
[GOAL]
case create
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ { l //
    l ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj
              WalkingParallelPair.zero},
        m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = l }
[PROOFSTEP]
refine' ⟨s.ι ≫ e, _⟩
[GOAL]
case create
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ (Fork.ι s ≫ e) ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s ∧
    ∀
      {m :
        ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
          ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero},
      m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = Fork.ι s ≫ e
[PROOFSTEP]
constructor
[GOAL]
case create.left
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ (Fork.ι s ≫ e) ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s
[PROOFSTEP]
erw [assoc, h₂, ← Limits.Fork.condition s, comp_id]
[GOAL]
case create.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ ∀
    {m :
      ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
        ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero},
    m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = Fork.ι s ≫ e
[PROOFSTEP]
intro m hm
[GOAL]
case create.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s
⊢ m = Fork.ι s ≫ e
[PROOFSTEP]
rw [Fork.ι_ofι] at hm
[GOAL]
case create.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ i = Fork.ι s
⊢ m = Fork.ι s ≫ e
[PROOFSTEP]
rw [← hm]
[GOAL]
case create.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ i = Fork.ι s
⊢ m = (m ≫ i) ≫ e
[PROOFSTEP]
simp only [← hm, assoc, h₁]
[GOAL]
case create.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ i = Fork.ι s
⊢ m = m ≫ 𝟙 Y
[PROOFSTEP]
exact (comp_id m).symm
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → IsIdempotentComplete C
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ IsIdempotentComplete C
[PROOFSTEP]
refine' ⟨_⟩
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
intro X p hp
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
haveI : HasEqualizer (𝟙 X) p := h X p hp
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
refine'
  ⟨equalizer (𝟙 X) p, equalizer.ι (𝟙 X) p, equalizer.lift p (show p ≫ 𝟙 X = p ≫ p by rw [hp, comp_id]), _,
    equalizer.lift_ι _ _⟩
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ p ≫ 𝟙 X = p ≫ p
[PROOFSTEP]
rw [hp, comp_id]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ equalizer.ι (𝟙 X) p ≫ equalizer.lift p (_ : p ≫ 𝟙 X = p ≫ p) = 𝟙 (equalizer (𝟙 X) p)
[PROOFSTEP]
ext
[GOAL]
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ (equalizer.ι (𝟙 X) p ≫ equalizer.lift p (_ : p ≫ 𝟙 X = p ≫ p)) ≫ equalizer.ι (𝟙 X) p =
    𝟙 (equalizer (𝟙 X) p) ≫ equalizer.ι (𝟙 X) p
[PROOFSTEP]
simp only [assoc, limit.lift_π, Eq.ndrec, id_eq, eq_mpr_eq_cast, Fork.ofι_pt, Fork.ofι_π_app, id_comp]
[GOAL]
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ equalizer.ι (𝟙 X) p ≫ p = equalizer.ι (𝟙 X) p
[PROOFSTEP]
rw [← equalizer.condition, comp_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ (𝟙 X - p) ≫ (𝟙 X - p) = 𝟙 X - p
[PROOFSTEP]
simp only [comp_sub, sub_comp, id_comp, comp_id, hp, sub_self, sub_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
⊢ IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
[PROOFSTEP]
rw [isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
[PROOFSTEP]
intro h X p hp
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasKernel p
[PROOFSTEP]
haveI : HasEqualizer (𝟙 X) (𝟙 X - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) (𝟙 X - p)
⊢ HasKernel p
[PROOFSTEP]
convert hasKernel_of_hasEqualizer (𝟙 X) (𝟙 X - p)
[GOAL]
case h.e'_6
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) (𝟙 X - p)
⊢ p = 𝟙 X - (𝟙 X - p)
[PROOFSTEP]
rw [sub_sub_cancel]
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
[PROOFSTEP]
intro h X p hp
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasEqualizer (𝟙 X) p
[PROOFSTEP]
haveI : HasKernel (𝟙 _ - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasKernel (𝟙 X - p)
⊢ HasEqualizer (𝟙 X) p
[PROOFSTEP]
apply Preadditive.hasEqualizer_of_hasKernel
[GOAL]
C : Type u_1
inst✝² : Category.{?u.11569, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.11576, u_2} D
inst✝ : Abelian D
⊢ IsIdempotentComplete D
[PROOFSTEP]
rw [isIdempotentComplete_iff_idempotents_have_kernels]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.11569, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.11576, u_2} D
inst✝ : Abelian D
⊢ ∀ (X : D) (p : X ⟶ X), p ≫ p = p → HasKernel p
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
inst✝² : Category.{?u.11569, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.11576, u_2} D
inst✝ : Abelian D
X✝ : D
p✝ : X✝ ⟶ X✝
a✝ : p✝ ≫ p✝ = p✝
⊢ HasKernel p✝
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
h : ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
[PROOFSTEP]
rcases h with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
[GOAL]
case intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
[PROOFSTEP]
use Y, i ≫ φ.hom, φ.inv ≫ e
[GOAL]
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ (i ≫ φ.hom) ≫ φ.inv ≫ e = 𝟙 Y ∧ (φ.inv ≫ e) ≫ i ≫ φ.hom = p'
[PROOFSTEP]
constructor
[GOAL]
case h.left
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ (i ≫ φ.hom) ≫ φ.inv ≫ e = 𝟙 Y
[PROOFSTEP]
slice_lhs 2 3 => rw [φ.hom_inv_id]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.hom ≫ φ.inv
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| e
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| i
[PROOFSTEP]
rw [φ.hom_inv_id]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.hom ≫ φ.inv
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| e
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| i
[PROOFSTEP]
rw [φ.hom_inv_id]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.hom ≫ φ.inv
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| e
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| i
[PROOFSTEP]
rw [φ.hom_inv_id]
[GOAL]
case h.left
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ i ≫ 𝟙 X ≫ e = 𝟙 Y
[PROOFSTEP]
rw [id_comp, h₁]
[GOAL]
case h.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ (φ.inv ≫ e) ≫ i ≫ φ.hom = p'
[PROOFSTEP]
slice_lhs 2 3 => rw [h₂]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| e ≫ i
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.hom
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.inv
[PROOFSTEP]
rw [h₂]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| e ≫ i
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.hom
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.inv
[PROOFSTEP]
rw [h₂]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| e ≫ i
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.hom
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
| φ.inv
[PROOFSTEP]
rw [h₂]
[GOAL]
case h.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ φ.inv ≫ p ≫ φ.hom = p'
[PROOFSTEP]
rw [hpp', ← assoc, φ.inv_hom_id, id_comp]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p) ↔ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p) → ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
[PROOFSTEP]
exact split_imp_of_iso φ p p' hpp'
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
apply split_imp_of_iso φ.symm p' p
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ p
[PROOFSTEP]
rw [← comp_id p, ← φ.hom_inv_id]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ p ≫ φ.hom ≫ φ.inv
[PROOFSTEP]
slice_rhs 2 3 => rw [hpp']
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| p ≫ φ.hom
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom
[PROOFSTEP]
rw [hpp']
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| p ≫ φ.hom
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom
[PROOFSTEP]
rw [hpp']
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| p ≫ φ.hom
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom
[PROOFSTEP]
rw [hpp']
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ (φ.hom ≫ p') ≫ φ.inv
[PROOFSTEP]
slice_rhs 1 2 => erw [φ.inv_hom_id]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom ≫ φ.hom
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| p'
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv
[PROOFSTEP]
erw [φ.inv_hom_id]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom ≫ φ.hom
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| p'
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv
[PROOFSTEP]
erw [φ.inv_hom_id]
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom ≫ φ.hom
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| p'
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv
[PROOFSTEP]
erw [φ.inv_hom_id]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = (𝟙 X' ≫ p') ≫ φ.inv
[PROOFSTEP]
simp only [id_comp]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = p' ≫ φ.inv
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
⊢ IsIdempotentComplete D
[PROOFSTEP]
refine' ⟨_⟩
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
⊢ ∀ (X : D) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
intro X' p hp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
let φ := ε.counitIso.symm.app X'
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
erw [split_iff_of_iso φ p (φ.inv ≫ p ≫ φ.hom)
    (by
      slice_rhs 1 2 => rw [φ.hom_inv_id]
      rw [id_comp])]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ p ≫ φ.hom = φ.hom ≫ φ.inv ≫ p ≫ φ.hom
[PROOFSTEP]
slice_rhs 1 2 => rw [φ.hom_inv_id]
[GOAL]
case a.a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom ≫ φ.inv
case a.a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| p
case a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom
[PROOFSTEP]
rw [φ.hom_inv_id]
[GOAL]
case a.a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom ≫ φ.inv
case a.a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| p
case a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom
[PROOFSTEP]
rw [φ.hom_inv_id]
[GOAL]
case a.a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom ≫ φ.inv
case a.a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| p
case a
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom
[PROOFSTEP]
rw [φ.hom_inv_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ p ≫ φ.hom = (𝟙 ((𝟭 D).obj X') ≫ p) ≫ φ.hom
[PROOFSTEP]
rw [id_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
[PROOFSTEP]
rcases IsIdempotentComplete.idempotents_split (ε.inverse.obj X') (ε.inverse.map p)
    (by rw [← ε.inverse.map_comp, hp]) with
  ⟨Y, i, e, ⟨h₁, h₂⟩⟩
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ε.inverse.map p ≫ ε.inverse.map p = ε.inverse.map p
[PROOFSTEP]
rw [← ε.inverse.map_comp, hp]
[GOAL]
case intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
[PROOFSTEP]
use ε.functor.obj Y, ε.functor.map i, ε.functor.map e
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y) ∧ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
[PROOFSTEP]
constructor
[GOAL]
case h.left
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)
[PROOFSTEP]
rw [← ε.functor.map_comp, h₁, ε.functor.map_id]
[GOAL]
case h.right
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
[PROOFSTEP]
simp only [← ε.functor.map_comp, h₂, Equivalence.fun_inv_map]
[GOAL]
case h.right
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ NatTrans.app (Equivalence.counit ε) X' ≫ p ≫ NatTrans.app (Equivalence.counitInv ε) X' =
    (ε.counitIso.symm.app X').inv ≫ p ≫ (ε.counitIso.symm.app X').hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete C ↔ IsIdempotentComplete D
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete C → IsIdempotentComplete D
[PROOFSTEP]
exact Equivalence.isIdempotentComplete ε
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete D → IsIdempotentComplete C
[PROOFSTEP]
exact Equivalence.isIdempotentComplete ε.symm
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
⊢ IsIdempotentComplete C
[PROOFSTEP]
refine' ⟨_⟩
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
intro X p hp
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
rcases IsIdempotentComplete.idempotents_split (op X) p.op (by rw [← op_comp, hp]) with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ p.op ≫ p.op = p.op
[PROOFSTEP]
rw [← op_comp, hp]
[GOAL]
case intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
[PROOFSTEP]
use Y.unop, e.unop, i.unop
[GOAL]
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 Y.unop ∧ i.unop ≫ e.unop = p
[PROOFSTEP]
constructor
[GOAL]
case h.left
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 Y.unop
[PROOFSTEP]
simp only [← unop_comp, h₁]
[GOAL]
case h.left
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ (𝟙 Y).unop = 𝟙 Y.unop
[PROOFSTEP]
rfl
[GOAL]
case h.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ i.unop ≫ e.unop = p
[PROOFSTEP]
simp only [← unop_comp, h₂]
[GOAL]
case h.right
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ p.op.unop = p
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ IsIdempotentComplete Cᵒᵖ ↔ IsIdempotentComplete C
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ IsIdempotentComplete Cᵒᵖ → IsIdempotentComplete C
[PROOFSTEP]
exact isIdempotentComplete_of_isIdempotentComplete_opposite
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ IsIdempotentComplete C → IsIdempotentComplete Cᵒᵖ
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete Cᵒᵖ
[PROOFSTEP]
apply isIdempotentComplete_of_isIdempotentComplete_opposite
[GOAL]
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete Cᵒᵖᵒᵖ
[PROOFSTEP]
rw [isIdempotentComplete_iff_of_equivalence (opOpEquivalence C)]
[GOAL]
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete C
[PROOFSTEP]
exact h
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.32276, u_1} C
inst✝ : IsIdempotentComplete C
⊢ IsIdempotentComplete Cᵒᵖ
[PROOFSTEP]
rwa [isIdempotentComplete_iff_opposite]


[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
⊢ Function.LeftInverse
    (fun γ =>
      {
        val :=
          sheafifyLift J
            (↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val).symm ((sheafToPresheaf J E).map γ))
            (_ : Presheaf.IsSheaf J Y.val) })
    fun η =>
    {
      val :=
        ↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val)
          (toSheafify J (((whiskeringRight Cᵒᵖ E D).obj G).obj ((sheafToPresheaf J E).obj X)) ≫ η.val) }
[PROOFSTEP]
intro η
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
η : (composeAndSheafify J G).obj X ⟶ Y
⊢ (fun γ =>
        {
          val :=
            sheafifyLift J
              (↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val).symm ((sheafToPresheaf J E).map γ))
              (_ : Presheaf.IsSheaf J Y.val) })
      ((fun η =>
          {
            val :=
              ↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val)
                (toSheafify J (((whiskeringRight Cᵒᵖ E D).obj G).obj ((sheafToPresheaf J E).obj X)) ≫ η.val) })
        η) =
    η
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
η : (composeAndSheafify J G).obj X ⟶ Y
⊢ ((fun γ =>
          {
            val :=
              sheafifyLift J
                (↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val).symm ((sheafToPresheaf J E).map γ))
                (_ : Presheaf.IsSheaf J Y.val) })
        ((fun η =>
            {
              val :=
                ↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val)
                  (toSheafify J (((whiskeringRight Cᵒᵖ E D).obj G).obj ((sheafToPresheaf J E).obj X)) ≫ η.val) })
          η)).val =
    η.val
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
η : (composeAndSheafify J G).obj X ⟶ Y
⊢ sheafifyLift J
      (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val).symm
        (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val) (toSheafify J (X.val ⋙ G) ≫ η.val)))
      (_ : Presheaf.IsSheaf J Y.val) =
    η.val
[PROOFSTEP]
symm
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
η : (composeAndSheafify J G).obj X ⟶ Y
⊢ η.val =
    sheafifyLift J
      (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val).symm
        (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val) (toSheafify J (X.val ⋙ G) ≫ η.val)))
      (_ : Presheaf.IsSheaf J Y.val)
[PROOFSTEP]
apply J.sheafifyLift_unique
[GOAL]
case h.a
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
η : (composeAndSheafify J G).obj X ⟶ Y
⊢ toSheafify J (X.val ⋙ G) ≫ η.val =
    ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val).symm
      (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val) (toSheafify J (X.val ⋙ G) ≫ η.val))
[PROOFSTEP]
rw [Equiv.symm_apply_apply]
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
⊢ Function.RightInverse
    (fun γ =>
      {
        val :=
          sheafifyLift J
            (↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val).symm ((sheafToPresheaf J E).map γ))
            (_ : Presheaf.IsSheaf J Y.val) })
    fun η =>
    {
      val :=
        ↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val)
          (toSheafify J (((whiskeringRight Cᵒᵖ E D).obj G).obj ((sheafToPresheaf J E).obj X)) ≫ η.val) }
[PROOFSTEP]
intro γ
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
γ : X ⟶ (sheafCompose J F).obj Y
⊢ (fun η =>
        {
          val :=
            ↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val)
              (toSheafify J (((whiskeringRight Cᵒᵖ E D).obj G).obj ((sheafToPresheaf J E).obj X)) ≫ η.val) })
      ((fun γ =>
          {
            val :=
              sheafifyLift J
                (↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val).symm ((sheafToPresheaf J E).map γ))
                (_ : Presheaf.IsSheaf J Y.val) })
        γ) =
    γ
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
γ : X ⟶ (sheafCompose J F).obj Y
⊢ ((fun η =>
          {
            val :=
              ↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val)
                (toSheafify J (((whiskeringRight Cᵒᵖ E D).obj G).obj ((sheafToPresheaf J E).obj X)) ≫ η.val) })
        ((fun γ =>
            {
              val :=
                sheafifyLift J
                  (↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val).symm ((sheafToPresheaf J E).map γ))
                  (_ : Presheaf.IsSheaf J Y.val) })
          γ)).val =
    γ.val
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
γ : X ⟶ (sheafCompose J F).obj Y
⊢ ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val)
      (toSheafify J (X.val ⋙ G) ≫
        sheafifyLift J (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val).symm γ.val)
          (_ : Presheaf.IsSheaf J Y.val)) =
    γ.val
[PROOFSTEP]
rw [J.toSheafify_sheafifyLift, Equiv.apply_symm_apply]
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X'✝ X✝ : Sheaf J E
Y✝ : Sheaf J D
f : X'✝ ⟶ X✝
g : X✝ ⟶ (sheafCompose J F).obj Y✝
⊢ ↑(composeEquiv J adj X'✝ Y✝).symm (f ≫ g) = (composeAndSheafify J G).map f ≫ ↑(composeEquiv J adj X✝ Y✝).symm g
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X'✝ X✝ : Sheaf J E
Y✝ : Sheaf J D
f : X'✝ ⟶ X✝
g : X✝ ⟶ (sheafCompose J F).obj Y✝
⊢ (↑(composeEquiv J adj X'✝ Y✝).symm (f ≫ g)).val =
    ((composeAndSheafify J G).map f ≫ ↑(composeEquiv J adj X✝ Y✝).symm g).val
[PROOFSTEP]
dsimp [composeEquiv]
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X'✝ X✝ : Sheaf J E
Y✝ : Sheaf J D
f : X'✝ ⟶ X✝
g : X✝ ⟶ (sheafCompose J F).obj Y✝
⊢ sheafifyLift J (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X'✝.val Y✝.val).symm (f.val ≫ g.val))
      (_ : Presheaf.IsSheaf J Y✝.val) =
    sheafifyMap J (whiskerRight f.val G) ≫
      sheafifyLift J (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y✝.val).symm g.val)
        (_ : Presheaf.IsSheaf J Y✝.val)
[PROOFSTEP]
rw [sheafifyMap_sheafifyLift]
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X'✝ X✝ : Sheaf J E
Y✝ : Sheaf J D
f : X'✝ ⟶ X✝
g : X✝ ⟶ (sheafCompose J F).obj Y✝
⊢ sheafifyLift J (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X'✝.val Y✝.val).symm (f.val ≫ g.val))
      (_ : Presheaf.IsSheaf J Y✝.val) =
    sheafifyLift J
      (whiskerRight f.val G ≫ ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y✝.val).symm g.val)
      (_ : Presheaf.IsSheaf J Y✝.val)
[PROOFSTEP]
erw [Adjunction.homEquiv_naturality_left_symm]
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X'✝ X✝ : Sheaf J E
Y✝ : Sheaf J D
f : X'✝ ⟶ X✝
g : X✝ ⟶ (sheafCompose J F).obj Y✝
⊢ sheafifyLift J
      (((whiskeringRight Cᵒᵖ E D).obj G).map f.val ≫
        ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y✝.val).symm g.val)
      (_ : Presheaf.IsSheaf J Y✝.val) =
    sheafifyLift J
      (whiskerRight f.val G ≫ ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y✝.val).symm g.val)
      (_ : Presheaf.IsSheaf J Y✝.val)
[PROOFSTEP]
rw [whiskeringRight_obj_map]
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X'✝ X✝ : Sheaf J E
Y✝ : Sheaf J D
f : X'✝ ⟶ X✝
g : X✝ ⟶ (sheafCompose J F).obj Y✝
⊢ sheafifyLift J
      (whiskerRight f.val G ≫ ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y✝.val).symm g.val)
      (_ : Presheaf.IsSheaf J Y✝.val) =
    sheafifyLift J
      (whiskerRight f.val G ≫ ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y✝.val).symm g.val)
      (_ : Presheaf.IsSheaf J Y✝.val)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X✝ : Sheaf J E
Y✝ Y'✝ : Sheaf J D
f : (composeAndSheafify J G).obj X✝ ⟶ Y✝
g : Y✝ ⟶ Y'✝
⊢ ↑(composeEquiv J adj X✝ Y'✝) (f ≫ g) = ↑(composeEquiv J adj X✝ Y✝) f ≫ (sheafCompose J F).map g
[PROOFSTEP]
ext
[GOAL]
case h.w.h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X✝ : Sheaf J E
Y✝ Y'✝ : Sheaf J D
f : (composeAndSheafify J G).obj X✝ ⟶ Y✝
g : Y✝ ⟶ Y'✝
x✝ : Cᵒᵖ
⊢ NatTrans.app (↑(composeEquiv J adj X✝ Y'✝) (f ≫ g)).val x✝ =
    NatTrans.app (↑(composeEquiv J adj X✝ Y✝) f ≫ (sheafCompose J F).map g).val x✝
[PROOFSTEP]
dsimp [composeEquiv]
[GOAL]
case h.w.h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X✝ : Sheaf J E
Y✝ Y'✝ : Sheaf J D
f : (composeAndSheafify J G).obj X✝ ⟶ Y✝
g : Y✝ ⟶ Y'✝
x✝ : Cᵒᵖ
⊢ NatTrans.app
      (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y'✝.val)
        (toSheafify J (X✝.val ⋙ G) ≫ f.val ≫ g.val))
      x✝ =
    NatTrans.app
        (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y✝.val) (toSheafify J (X✝.val ⋙ G) ≫ f.val))
        x✝ ≫
      F.map (NatTrans.app g.val x✝)
[PROOFSTEP]
erw [Adjunction.homEquiv_unit, Adjunction.homEquiv_unit]
[GOAL]
case h.w.h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X✝ : Sheaf J E
Y✝ Y'✝ : Sheaf J D
f : (composeAndSheafify J G).obj X✝ ⟶ Y✝
g : Y✝ ⟶ Y'✝
x✝ : Cᵒᵖ
⊢ NatTrans.app
      (NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).unit X✝.val ≫
        ((whiskeringRight Cᵒᵖ D E).obj F).map (toSheafify J (X✝.val ⋙ G) ≫ f.val ≫ g.val))
      x✝ =
    NatTrans.app
        (NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).unit X✝.val ≫
          ((whiskeringRight Cᵒᵖ D E).obj F).map (toSheafify J (X✝.val ⋙ G) ≫ f.val))
        x✝ ≫
      F.map (NatTrans.app g.val x✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.w.h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X✝ : Sheaf J E
Y✝ Y'✝ : Sheaf J D
f : (composeAndSheafify J G).obj X✝ ⟶ Y✝
g : Y✝ ⟶ Y'✝
x✝ : Cᵒᵖ
⊢ NatTrans.app (NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).unit X✝.val) x✝ ≫
      F.map (NatTrans.app (toSheafify J (X✝.val ⋙ G)) x✝ ≫ NatTrans.app f.val x✝ ≫ NatTrans.app g.val x✝) =
    (NatTrans.app (NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).unit X✝.val) x✝ ≫
        F.map (NatTrans.app (toSheafify J (X✝.val ⋙ G)) x✝ ≫ NatTrans.app f.val x✝)) ≫
      F.map (NatTrans.app g.val x✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
Y : SheafOfTypes J
⊢ (NatTrans.app (adjunctionToTypes J adj).unit Y).val =
    NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).unit ((sheafOfTypesToPresheaf J).obj Y) ≫
      whiskerRight
        (toSheafify J (((whiskeringRight Cᵒᵖ (Type (max v u)) D).obj G).obj ((sheafOfTypesToPresheaf J).obj Y)))
        (forget D)
[PROOFSTEP]
dsimp [adjunctionToTypes, Adjunction.comp]
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
Y : SheafOfTypes J
⊢ (NatTrans.app (Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).unit Y).val ≫
      (NatTrans.app (adjunction J adj).unit ((sheafEquivSheafOfTypes J).inverse.obj Y)).val ≫
        𝟙 (sheafify J (Y.val ⋙ G) ⋙ forget D) =
    NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).unit Y.val ≫ whiskerRight (toSheafify J (Y.val ⋙ G)) (forget D)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
Y : SheafOfTypes J
⊢ (NatTrans.app (Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).unit Y).val ≫
      ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Y.val (sheafify J (Y.val ⋙ G)))
        (toSheafify J (Y.val ⋙ G)) =
    NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).unit Y.val ≫ whiskerRight (toSheafify J (Y.val ⋙ G)) (forget D)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
X : Sheaf J D
⊢ (NatTrans.app (adjunctionToTypes J adj).counit X).val =
    sheafifyLift J
      ((Functor.associator X.1 (forget D) G).hom ≫ NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).counit X.1)
      (_ : Presheaf.IsSheaf J X.val)
[PROOFSTEP]
apply J.sheafifyLift_unique
[GOAL]
case a
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
X : Sheaf J D
⊢ toSheafify J
        (((whiskeringRight Cᵒᵖ (Type (max u v)) D).obj G).obj
          ((sheafToPresheaf J (Type (max u v))).obj ((sheafEquivSheafOfTypes J).inverse.obj ((sheafForget J).obj X)))) ≫
      (NatTrans.app (adjunctionToTypes J adj).counit X).val =
    (Functor.associator X.1 (forget D) G).hom ≫ NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).counit X.1
[PROOFSTEP]
dsimp only [adjunctionToTypes, Adjunction.comp, NatTrans.comp_app, instCategorySheaf_comp_val, instCategorySheaf_id_val]
[GOAL]
case a
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
X : Sheaf J D
⊢ toSheafify J
        (((whiskeringRight Cᵒᵖ (Type (max u v)) D).obj G).obj
          ((sheafToPresheaf J (Type (max u v))).obj ((sheafEquivSheafOfTypes J).inverse.obj ((sheafForget J).obj X)))) ≫
      (NatTrans.app
            (Functor.associator (sheafCompose J (forget D)) (Equivalence.symm (sheafEquivSheafOfTypes J)).inverse
                ((Equivalence.symm (sheafEquivSheafOfTypes J)).functor ⋙ composeAndSheafify J G)).hom
            X).val ≫
        (NatTrans.app
              (whiskerLeft (sheafCompose J (forget D))
                (whiskerRight (Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).counit
                  (composeAndSheafify J G)))
              X).val ≫
          (NatTrans.app (adjunction J adj).counit X).val =
    (Functor.associator X.1 (forget D) G).hom ≫ NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).counit X.1
[PROOFSTEP]
rw [adjunction_counit_app_val]
[GOAL]
case a
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
X : Sheaf J D
⊢ toSheafify J
        (((whiskeringRight Cᵒᵖ (Type (max u v)) D).obj G).obj
          ((sheafToPresheaf J (Type (max u v))).obj ((sheafEquivSheafOfTypes J).inverse.obj ((sheafForget J).obj X)))) ≫
      (NatTrans.app
            (Functor.associator (sheafCompose J (forget D)) (Equivalence.symm (sheafEquivSheafOfTypes J)).inverse
                ((Equivalence.symm (sheafEquivSheafOfTypes J)).functor ⋙ composeAndSheafify J G)).hom
            X).val ≫
        (NatTrans.app
              (whiskerLeft (sheafCompose J (forget D))
                (whiskerRight (Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).counit
                  (composeAndSheafify J G)))
              X).val ≫
          sheafifyLift J
            (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) (X.val ⋙ forget D) X.val).symm
              (𝟙 (X.val ⋙ forget D)))
            (_ : Presheaf.IsSheaf J X.val) =
    (Functor.associator X.1 (forget D) G).hom ≫ NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).counit X.1
[PROOFSTEP]
erw [Category.id_comp, J.sheafifyMap_sheafifyLift, J.toSheafify_sheafifyLift]
[GOAL]
case a
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
X : Sheaf J D
⊢ ((whiskeringRight Cᵒᵖ (Type (max u v)) D).obj G).map
        ((sheafToPresheaf J (Type (max u v))).map
          (NatTrans.app (Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).counit
            ((sheafCompose J (forget D)).obj X))) ≫
      ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) (X.val ⋙ forget D) X.val).symm (𝟙 (X.val ⋙ forget D)) =
    (Functor.associator X.1 (forget D) G).hom ≫ NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).counit X.1
[PROOFSTEP]
ext
[GOAL]
case a.w.h.w
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
X : Sheaf J D
x✝¹ : Cᵒᵖ
x✝ :
  (forget D).obj
    ((((whiskeringRight Cᵒᵖ (Type (max u v)) D).obj G).obj
          ((sheafToPresheaf J (Type (max u v))).obj
            (((Equivalence.symm (sheafEquivSheafOfTypes J)).inverse ⋙
                  (Equivalence.symm (sheafEquivSheafOfTypes J)).functor).obj
              ((sheafCompose J (forget D)).obj X)))).obj
      x✝¹)
⊢ ↑(NatTrans.app
          (((whiskeringRight Cᵒᵖ (Type (max u v)) D).obj G).map
              ((sheafToPresheaf J (Type (max u v))).map
                (NatTrans.app (Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).counit
                  ((sheafCompose J (forget D)).obj X))) ≫
            ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) (X.val ⋙ forget D) X.val).symm
              (𝟙 (X.val ⋙ forget D)))
          x✝¹)
      x✝ =
    ↑(NatTrans.app
          ((Functor.associator X.1 (forget D) G).hom ≫ NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).counit X.1) x✝¹)
      x✝
[PROOFSTEP]
dsimp [sheafEquivSheafOfTypes, Equivalence.symm, Equivalence.toAdjunction, NatIso.ofComponents, Adjunction.whiskerRight,
  Adjunction.mkOfUnitCounit]
[GOAL]
case a.w.h.w
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
X : Sheaf J D
x✝¹ : Cᵒᵖ
x✝ :
  (forget D).obj
    ((((whiskeringRight Cᵒᵖ (Type (max u v)) D).obj G).obj
          ((sheafToPresheaf J (Type (max u v))).obj
            (((Equivalence.symm (sheafEquivSheafOfTypes J)).inverse ⋙
                  (Equivalence.symm (sheafEquivSheafOfTypes J)).functor).obj
              ((sheafCompose J (forget D)).obj X)))).obj
      x✝¹)
⊢ ↑(G.map (𝟙 ((forget D).obj (X.val.obj x✝¹))) ≫
          G.map (𝟙 ((forget D).obj (X.val.obj x✝¹))) ≫
            𝟙 (G.obj ((forget D).obj (X.val.obj x✝¹))) ≫ NatTrans.app adj.counit (X.val.obj x✝¹) ≫ 𝟙 (X.val.obj x✝¹))
      x✝ =
    ↑(𝟙 (G.obj ((forget D).obj (X.1.obj x✝¹))) ≫
          𝟙 (G.obj ((forget D).obj (X.1.obj x✝¹))) ≫ NatTrans.app adj.counit (X.1.obj x✝¹) ≫ 𝟙 (X.val.obj x✝¹))
      x✝
[PROOFSTEP]
simp


[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ HomologicalComplex.Hom.f I.ι (n + 1) = 0
[PROOFSTEP]
apply zero_of_source_iso_zero
[GOAL]
case i
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ HomologicalComplex.X ((CochainComplex.single₀ C).obj Z) (n + 1) ≅ 0
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ Mono (HomologicalComplex.Hom.f I.ι n)
[PROOFSTEP]
cases n
[GOAL]
case zero
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
I : InjectiveResolution Z
⊢ Mono (HomologicalComplex.Hom.f I.ι Nat.zero)
[PROOFSTEP]
apply I.mono
[GOAL]
case succ
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
I : InjectiveResolution Z
n✝ : ℕ
⊢ Mono (HomologicalComplex.Hom.f I.ι (Nat.succ n✝))
[PROOFSTEP]
rw [ι_f_succ]
[GOAL]
case succ
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
I : InjectiveResolution Z
n✝ : ℕ
⊢ Mono 0
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
n : ℕ
⊢ Injective (HomologicalComplex.X ((CochainComplex.single₀ C).obj Z) n)
[PROOFSTEP]
cases n
[GOAL]
case zero
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
⊢ Injective (HomologicalComplex.X ((CochainComplex.single₀ C).obj Z) Nat.zero)
[PROOFSTEP]
dsimp
[GOAL]
case zero
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
⊢ Injective Z
[PROOFSTEP]
infer_instance
[GOAL]
case succ
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
n✝ : ℕ
⊢ Injective (HomologicalComplex.X ((CochainComplex.single₀ C).obj Z) (Nat.succ n✝))
[PROOFSTEP]
dsimp
[GOAL]
case succ
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
n✝ : ℕ
⊢ Injective 0
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
⊢ Exact (HomologicalComplex.Hom.f (𝟙 ((CochainComplex.single₀ C).obj Z)) 0)
    (HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) 0 1)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
⊢ Exact (𝟙 Z) 0
[PROOFSTEP]
exact exact_epi_zero _
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
n : ℕ
⊢ Exact (HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) n (n + 1))
    (HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) (n + 1) (n + 2))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
n : ℕ
⊢ Exact 0 0
[PROOFSTEP]
exact exact_of_zero _ _
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
⊢ Mono (HomologicalComplex.Hom.f (𝟙 ((CochainComplex.single₀ C).obj Z)) 0)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
⊢ Mono (𝟙 Z)
[PROOFSTEP]
infer_instance