awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
II : (unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).shape.L
⊢ Eq (α :=
    multiequalizer ((unop S).index P) ⟶
      ((unop S).index P).right
        (Cover.Relation.mk (snd := Cover.Arrow.base II) { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ }))
    (Multiequalizer.ι ((unop S).index P)
        ((unop S).shape.fst
          (Cover.Relation.mk (snd := Cover.Arrow.base II) { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ })) ≫
      ((unop S).index P).fst
        (Cover.Relation.mk (snd := Cover.Arrow.base II)
          { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ : Cover.Arrow.Relation I (Cover.Arrow.base II) }))
    (Multiequalizer.ι ((unop S).index P)
        ((unop S).shape.snd
          (Cover.Relation.mk (snd := Cover.Arrow.base II) { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ })) ≫
      ((unop S).index P).snd
        (Cover.Relation.mk (snd := Cover.Arrow.base II)
          { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ : Cover.Arrow.Relation I (Cover.Arrow.base II) }))

Tactic:
Multiequalizer.condition (S.unop.index P)
      { fst := I, snd := II.base, r.Z := II.Y, r.g₁ := II.f, r.g₂ := 𝟙 II.Y }

Premises used: CategoryTheory.Limits.Multiequalizer.condition, CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.mk, CategoryTheory.CategoryStruct.id, CategoryTheory.GrothendieckTopology.Cover.index, CategoryTheory.GrothendieckTopology.Cover.Relation.mk, CategoryTheory.GrothendieckTopology.Cover.Arrow.f, CategoryTheory.GrothendieckTopology.Cover.Arrow.Y, Opposite.unop
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
II : (unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).shape.L
e_1 :
  (Functor.obj (J.diagram P (unop X)) S ⟶
      ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P).left II) =
    (multiequalizer ((unop S).index P) ⟶
      ((unop S).index P).right
        (Cover.Relation.mk (snd := Cover.Arrow.base II) { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ }))
⊢ Eq (α :=
    Functor.obj (J.diagram P (unop X)) S ⟶
      ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P).left II)
    (CategoryStruct.comp (Y := multiequalizer ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P))
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
        (Multiequalizer.ι ((unop S).index P) I ≫ Cover.toMultiequalizer ⊤ P) (Functor.map (J.diagram P I.Y) ee.op))
      (Multiequalizer.ι ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P) II))
    (Multiequalizer.ι ((unop S).index P)
        ((unop S).shape.fst
          (Cover.Relation.mk (snd := Cover.Arrow.base II) { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ })) ≫
      ((unop S).index P).fst
        (Cover.Relation.mk (snd := Cover.Arrow.base II)
          { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ : Cover.Arrow.Relation I (Cover.Arrow.base II) }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
II : (unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).shape.L
e_1 :
  (Functor.obj (J.diagram P (unop X)) S ⟶
      ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P).left II) =
    (multiequalizer ((unop S).index P) ⟶
      ((unop S).index P).right
        (Cover.Relation.mk (snd := Cover.Arrow.base II) { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ }))
⊢ Eq (α :=
    Functor.obj (J.diagram P (unop X)) S ⟶
      ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P).left II)
    (CategoryStruct.comp (Y := multiequalizer ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P))
      (Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
        (Functor.obj (J.diagram P (unop X)) S)
        (fun (I_1 : (unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).shape.L) ↦
          Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I_1))
        ⋯)
      (Multiequalizer.ι ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P) II))
    (Multiequalizer.ι ((unop S).index P)
        ((unop S).shape.snd
          (Cover.Relation.mk (snd := Cover.Arrow.base II) { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ })) ≫
      ((unop S).index P).snd
        (Cover.Relation.mk (snd := Cover.Arrow.base II)
          { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ : Cover.Arrow.Relation I (Cover.Arrow.base II) }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)

Tactic:
rw [Presheaf.isSheaf_iff_multiequalizer] at hP

Premises used: CategoryTheory.Presheaf.isSheaf_iff_multiequalizer
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
suffices : ∀ (X : Cᵒᵖ), IsIso (Y := (J.plusObj P).obj X) (NatTrans.app (J.toPlus P) X)
⊢ IsIso (Y := J.plusObj P) (J.toPlus P)

Tactic:
suffices ∀ X, IsIso ((J.toPlus P).app X) from NatIso.isIso_of_isIso_app _
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
X : Cᵒᵖ
⊢ IsIso (Y := (J.plusObj P).obj X) (NatTrans.app (J.toPlus P) X)

Tactic:
IsIso.comp_isIso' inferInstance ?_

Premises used: inferInstance, CategoryTheory.IsIso.comp_isIso'
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
X : Cᵒᵖ
refine :
  IsIso (X := multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ P)) (Y :=
    (J.plusObj P).obj X)
    (colimit.ι (J.diagram P (unop X)) (op ⊤) :
      Functor.obj (C := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)) (op ⊤) ⟶
        colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
⊢ IsIso (Y := (J.plusObj P).obj X) (NatTrans.app (J.toPlus P) X)

Tactic:
refine IsIso.comp_isIso' inferInstance ?_

Premises used: inferInstance, CategoryTheory.IsIso.comp_isIso'
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
X : Cᵒᵖ
suffices :
  ∀ (S T : (J.Cover (unop X))ᵒᵖ) (f : S ⟶ T),
    IsIso (X := Functor.obj (J.diagram P (unop X)) S) (Functor.map (J.diagram P (unop X)) f)
⊢ IsIso (X := multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ P)) (Y :=
    (J.plusObj P).obj X)
    (colimit.ι (J.diagram P (unop X)) (op ⊤) :
      Functor.obj (C := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)) (op ⊤) ⟶
        colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))

Tactic:
suffices ∀ (S T : (J.Cover X.unop)ᵒᵖ) (f : S ⟶ T), IsIso ((J.diagram P X.unop).map f) from
    isIso_ι_of_isInitial (initialOpOfTerminal isTerminalTop) _
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
X : Cᵒᵖ
S T : (J.Cover (unop X))ᵒᵖ
e : S ⟶ T
II : (unop T).shape.L
⊢ CategoryStruct.comp (Y := multiequalizer ((unop T).index P))
      (CategoryStruct.comp (Y := multiequalizer ((unop S).index P)) ((unop S).toMultiequalizer P)
        (Functor.map (J.diagram P (unop X)) e))
      (Multiequalizer.ι ((unop T).index P) II) =
    CategoryStruct.comp (Y := multiequalizer ((unop T).index P)) ((unop T).toMultiequalizer P)
      (Multiequalizer.ι ((unop T).index P) II)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
X : Cᵒᵖ
S T : (J.Cover (unop X))ᵒᵖ
e : S ⟶ T
⊢ Eq (α := P.obj (op (unop X)) ⟶ Functor.obj (J.diagram P (unop X)) T)
    (CategoryStruct.comp (Y := multiequalizer ((unop S).index P)) ((unop S).toMultiequalizer P)
      (Functor.map (J.diagram P (unop X)) e))
    ((unop T).toMultiequalizer P)

Tactic:
have : S.unop.toMultiequalizer P ≫ (J.diagram P X.unop).map e = T.unop.toMultiequalizer P :=
    Multiequalizer.hom_ext _ _ _ (fun II => by simp)
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
X : Cᵒᵖ
S T : (J.Cover (unop X))ᵒᵖ
e : S ⟶ T
this :
  Eq (α := P.obj (op (unop X)) ⟶ Functor.obj (J.diagram P (unop X)) T)
    (CategoryStruct.comp (Y := multiequalizer ((unop S).index P)) ((unop S).toMultiequalizer P)
      (Functor.map (J.diagram P (unop X)) e))
    ((unop T).toMultiequalizer P)
⊢ IsIso (X := Functor.obj (J.diagram P (unop X)) S) (Functor.map (J.diagram P (unop X)) e)

Tactic:
IsIso.of_isIso_fac_left this

Premises used: CategoryTheory.IsIso.of_isIso_fac_left
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
X : Cᵒᵖ
S T : (J.Cover (unop X))ᵒᵖ
e : S ⟶ T
this :
  Eq (α := P.obj (op (unop X)) ⟶ Functor.obj (J.diagram P (unop X)) T)
    (CategoryStruct.comp (Y := multiequalizer ((unop S).index P)) ((unop S).toMultiequalizer P)
      (Functor.map (J.diagram P (unop X)) e))
    ((unop T).toMultiequalizer P)
⊢ IsIso (X := Functor.obj (J.diagram P (unop X)) S) (Functor.map (J.diagram P (unop X)) e)

Tactic:
exact IsIso.of_isIso_fac_left this

Premises used: CategoryTheory.IsIso.of_isIso_fac_left
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ Eq (α := P ⟶ J.plusObj P) (Iso.hom (J.isoToPlus P hP)) (J.toPlus P)

Tactic:
rfl

Premises used: CategoryTheory.GrothendieckTopology.toPlus, rfl
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
rw : CategoryStruct.comp (Y := J.plusObj Q) (J.toPlus P ≫ J.plusMap η) (Iso.inv (J.isoToPlus Q hQ)) = η
⊢ CategoryStruct.comp (Y := J.plusObj P) (J.toPlus P) (J.plusMap η ≫ Iso.inv (J.isoToPlus Q hQ)) = η

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
rw : Eq (α := P ⟶ J.plusObj Q) (J.toPlus P ≫ J.plusMap η) (η ≫ Iso.hom (J.isoToPlus Q hQ))
⊢ CategoryStruct.comp (Y := J.plusObj Q) (J.toPlus P ≫ J.plusMap η) (Iso.inv (J.isoToPlus Q hQ)) = η

Tactic:
rw [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
rw rw₁ : Eq (α := P ⟶ J.plusObj Q) (J.toPlus P ≫ J.plusMap η) (J.toPlus P ≫ J.plusMap η)
⊢ Eq (α := P ⟶ J.plusObj Q) (J.toPlus P ≫ J.plusMap η) (η ≫ J.toPlus Q)

Tactic:
rw [toPlus_naturality]

Premises used: CategoryTheory.GrothendieckTopology.toPlus_naturality
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.plusObj P ⟶ Q
hγ : J.toPlus P ≫ γ = η
rw : γ ≫ Iso.hom (J.isoToPlus Q hQ) = J.plusMap (J.toPlus P) ≫ J.plusMap γ
⊢ γ = J.plusMap η ≫ Iso.inv (J.isoToPlus Q hQ)

Tactic:
rw [Iso.eq_comp_inv, ← hγ, plusMap_comp]

Premises used: CategoryTheory.Iso.eq_comp_inv, CategoryTheory.GrothendieckTopology.plusMap_comp
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.plusObj P ⟶ Q
hγ : J.toPlus P ≫ γ = η
⊢ γ ≫ Iso.hom (J.isoToPlus Q hQ) = J.plusMap (J.toPlus P) ≫ J.plusMap γ

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η γ : J.plusObj P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toPlus P ≫ η = J.toPlus P ≫ γ
hγ : J.toPlus P ≫ γ = J.toPlus P ≫ γ
⊢ γ = J.plusLift (J.toPlus P ≫ γ) hQ

Tactic:
apply plusLift_unique

Premises used: CategoryTheory.GrothendieckTopology.plusLift_unique
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η γ : J.plusObj P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toPlus P ≫ η = J.toPlus P ≫ γ
⊢ J.toPlus P ≫ γ = J.toPlus P ≫ γ

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η γ : J.plusObj P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toPlus P ≫ η = J.toPlus P ≫ γ
⊢ γ = J.plusLift (J.toPlus P ≫ γ) hQ

Tactic:
have : γ = J.plusLift (J.toPlus P ≫ γ) hQ := by
    apply plusLift_unique
    rfl
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η γ : J.plusObj P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toPlus P ≫ η = J.toPlus P ≫ γ
this : γ = J.plusLift (J.toPlus P ≫ γ) hQ
rw : η = J.plusLift (J.toPlus P ≫ γ) hQ
⊢ η = γ

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η γ : J.plusObj P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toPlus P ≫ η = J.toPlus P ≫ γ
this : γ = J.plusLift (J.toPlus P ≫ γ) hQ
hγ : J.toPlus P ≫ η = J.toPlus P ≫ γ
⊢ η = J.plusLift (J.toPlus P ≫ γ) hQ

Tactic:
apply plusLift_unique

Premises used: CategoryTheory.GrothendieckTopology.plusLift_unique
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η γ : J.plusObj P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toPlus P ≫ η = J.toPlus P ≫ γ
this : γ = J.plusLift (J.toPlus P ≫ γ) hQ
⊢ J.toPlus P ≫ η = J.toPlus P ≫ γ

Tactic:
h
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η γ : J.plusObj P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toPlus P ≫ η = J.toPlus P ≫ γ
this : γ = J.plusLift (J.toPlus P ≫ γ) hQ
⊢ J.toPlus P ≫ η = J.toPlus P ≫ γ

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
hγ : CategoryStruct.comp (Y := J.plusObj P) (J.toPlus P) (Iso.inv (J.isoToPlus P hP)) = 𝟙 P
⊢ Eq (α := J.plusObj P ⟶ P) (Iso.inv (J.isoToPlus P hP)) (J.plusLift (𝟙 P) hP)

Tactic:
apply J.plusLift_unique

Premises used: CategoryTheory.GrothendieckTopology.plusLift_unique
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
hγ : Eq (α := P ⟶ J.plusObj P) (J.toPlus P) (Iso.hom (J.isoToPlus P hP))
⊢ CategoryStruct.comp (Y := J.plusObj P) (J.toPlus P) (Iso.inv (J.isoToPlus P hP)) = 𝟙 P

Tactic:
rw [Iso.comp_inv_eq, Category.id_comp]

Premises used: CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ Eq (α := P ⟶ J.plusObj P) (J.toPlus P) (Iso.hom (J.isoToPlus P hP))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
hγ : CategoryStruct.comp (Y := J.plusObj P) (J.toPlus P) (J.plusMap η ≫ J.plusLift γ hR) = η ≫ γ
⊢ Eq (α := J.plusObj P ⟶ R) (J.plusMap η ≫ J.plusLift γ hR) (J.plusLift (η ≫ γ) hR)

Tactic:
apply J.plusLift_unique

Premises used: CategoryTheory.GrothendieckTopology.plusLift_unique