mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
j : β
k : α
h : ¬f k = g j
⊢ 0 = biproduct.ι (fun a ↦ s (f a)) k ≫ z ≫ biproduct.π (fun b ↦ s (g b)) j

Tactic:
· symm
      apply o.eq_zero h

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Adjunction

Goal state before:
pp: C : Type u
D : Type u'
inst✝² : Category.{v, u} C
inst✝¹ : Category.{v', u'} D
e : C ≌ D
inst✝ : IsLocallyPresentable.{w, v, u} C
⊢ IsLocallyPresentable.{w, v', u'} D

Tactic:
obtain ⟨κ, _, _⟩ := IsLocallyPresentable.exists_cardinal.{w} C
  exact ⟨κ, inferInstance, e.isCardinalLocallyPresentable κ⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ (M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N'.X) ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft))
            WalkingParallelPair.one) ▷
        P.X ≫
      colimit.ι
        (parallelPair (TensorBimod.actRight M N' ▷ P.X)
          ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
        WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      M.X ◁
          (f.hom ▷ P.X ≫
            colimit.ι (parallelPair (N'.actRight ▷ P.X) ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft))
              WalkingParallelPair.one) ≫
        (PreservesCoequalizer.iso (tensorLeft M.X) (N'.actRight ▷ P.X) ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft)).inv ≫
          coequalizer.desc
            ((α_ M.X N'.X P.X).inv ≫
              coequalizer.π (M.actRight ▷ N'.X) ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft) ▷ P.X ≫
                coequalizer.π (TensorBimod.actRight M N' ▷ P.X)
                  ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
            ⋯

Tactic:
slice_rhs 2 2 => rw [whiskerLeft_comp]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ (M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N'.X) ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft))
            WalkingParallelPair.one) ▷
        P.X ≫
      colimit.ι
        (parallelPair (TensorBimod.actRight M N' ▷ P.X)
          ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
        WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      ((M.X ◁ f.hom ▷ P.X ≫
            M.X ◁
              colimit.ι (parallelPair (N'.actRight ▷ P.X) ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft))
                WalkingParallelPair.one) ≫
          (PreservesCoequalizer.iso (tensorLeft M.X) (N'.actRight ▷ P.X)
              ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft)).inv) ≫
        coequalizer.desc
          ((α_ M.X N'.X P.X).inv ≫
            coequalizer.π (M.actRight ▷ N'.X) ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft) ▷ P.X ≫
              coequalizer.π (TensorBimod.actRight M N' ▷ P.X)
                ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
          ⋯
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{u, u, u + 1} Q), hasCardinalLTWithTerminal κ ≤ Q.isoClosure

Tactic:
by
    obtain ⟨X, hX⟩ : ∃ (X : Type u), Cardinal.mk X = κ := ⟨κ.ord.ToType, by simp⟩
    let α : Type u := Σ (S : Set X) (_ : PartialOrder S),
      ULift.{u} (PLift (IsCardinalFiltered S κ))
    let (a : α) : PartialOrder a.1 := a.2.1
    let ι (a : α) : CardinalDirectedPoset κ :=
      { obj := .of a.1
        property := a.2.2.down.down }
    refine ⟨.ofObj ι, inferInstance, fun J ⟨hJ, _⟩ ↦ ?_⟩
    obtain ⟨f⟩ : Cardinal.mk J.obj ≤ Cardinal.mk X := by
      simpa [hX] using ((hasCardinalLT_iff_cardinal_mk_lt _ _).1 hJ).le
    let e := Equiv.ofInjective _ f.injective
    let : PartialOrder (Set.range f) := PartialOrder.lift _ e.symm.injective
    let e' : Set.range f ≃o J.obj := { toEquiv := e.symm, map_rel_iff' := by rfl }
    exact ⟨_, ⟨⟨Set.range f, inferInstance,
      ⟨⟨IsCardinalFiltered.of_equivalence κ e'.symm.equivalence⟩⟩⟩⟩,
        ⟨CardinalDirectedPoset.ι.preimageIso (PartOrdEmb.Iso.mk (by exact e'.symm))⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
⊢ IsColimit ((coyoneda.obj (Opposite.op J)).mapCocone c)

Tactic:
refine Types.FilteredColimit.isColimitOf' _ _ (fun f ↦ ?_) (fun j f g h ↦ ?_)

Goal state after:
case refine_1
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
f : ((coyoneda.obj (Opposite.op J)).mapCocone c).pt
⊢ ∃ i xi, f = (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app i)) xi

case refine_2
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h✝ : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
j : A
f g : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op J)).obj j)
h :
  (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app j)) f =
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app j)) g
⊢ ∃ k f_1,
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op J)).map f_1)) f =
      (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op J)).map f_1)) g
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case hW
J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
x✝¹ x✝ : DiagramWithUniqueTerminal J κ
h₁ : x✝¹.W ≤ x✝.W ∧ x✝¹.P ≤ x✝.P
h₂ : x✝.W ≤ x✝¹.W ∧ x✝.P ≤ x✝¹.P
⊢ x✝¹.W = x✝.W

pp: case hP
J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
x✝¹ x✝ : DiagramWithUniqueTerminal J κ
h₁ : x✝¹.W ≤ x✝.W ∧ x✝¹.P ≤ x✝.P
h₂ : x✝.W ≤ x✝¹.W ∧ x✝.P ≤ x✝¹.P
⊢ x✝¹.P = x✝.P

Tactic:
· exact le_antisymm h₁.1 h₂.1

Goal state after:
case hP
J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
x✝¹ x✝ : DiagramWithUniqueTerminal J κ
h₁ : x✝¹.W ≤ x✝.W ∧ x✝¹.P ≤ x✝.P
h₂ : x✝.W ≤ x✝¹.W ∧ x✝.P ≤ x✝¹.P
⊢ x✝¹.P = x✝.P
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
j : ↑J.obj
this : OrderTop ↑{j} := { top := ⟨j, ⋯⟩, le_top := ⋯ }
⊢ HasTerminal ↑{j}

Tactic:
exact isTerminalTop.hasTerminal

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h : κ₁ ≤ κ₂
inst✝ : IsCardinalAccessibleCategory (CardinalDirectedPoset κ₁) κ₂
X : Type w
hX : HasCardinalLT X κ₂
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ₂
p : (isCardinalPresentable (CardinalDirectedPoset κ₁) κ₂).ColimitOfShape J (setCardinalLT κ₁ X)
this : IsCardinalFiltered J κ₁
⊢ ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y

Tactic:
have hp (j : J) : HasCardinalLT (p.diag.obj j).obj κ₂ := by
    rw [← CardinalDirectedPoset.isCardinalPresentable_iff _ h]
    exact p.prop_diag_obj j

Goal state after:
κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h : κ₁ ≤ κ₂
inst✝ : IsCardinalAccessibleCategory (CardinalDirectedPoset κ₁) κ₂
X : Type w
hX : HasCardinalLT X κ₂
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ₂
p : (isCardinalPresentable (CardinalDirectedPoset κ₁) κ₂).ColimitOfShape J (setCardinalLT κ₁ X)
this : IsCardinalFiltered J κ₁
hp : ∀ (j : J), HasCardinalLT (↑(p.diag.obj j).obj) κ₂
⊢ ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h : κ₁ ≤ κ₂
inst✝ : IsCardinalAccessibleCategory (CardinalDirectedPoset κ₁) κ₂
X : Type w
hX : HasCardinalLT X κ₂
⊢ ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y

Tactic:
by
  -- We write the partially ordered type `SetCardinalLT κ₁ X` of subsets
  -- of `X` of cardinality `< κ₁` as a `κ₂`-filtered colimit (with index
  -- category `J`) of `κ₂`-presentable objects (i.e. partially ordered
  -- types of cardinality `< κ₂`.)
  obtain ⟨J, _, _, ⟨p⟩⟩ := (isCardinalFilteredGenerator_isCardinalPresentable
    (CardinalDirectedPoset κ₁) κ₂).exists_colimitsOfShape (setCardinalLT κ₁ X)
  have : IsCardinalFiltered J κ₁ := .of_le _ h
  have hp (j : J) : HasCardinalLT (p.diag.obj j).obj κ₂ := by
    rw [← CardinalDirectedPoset.isCardinalPresentable_iff _ h]
    exact p.prop_diag_obj j
  -- For each `x : X`, we choose `j : J` in such a way that the singleton
  -- `{x}` belongs to the image of `p.diag.obj j` in `SetCardinalLT κ₁ X`.
  choose j y hy using fun x ↦ Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves (forget (CardinalDirectedPoset κ₁)) p.isColimit)
    (SetCardinalLT.singleton κ₁ x)
  dsimp at y hy
  -- The expected cofinal set `A` will be the range of `p.ι.app j'`
  -- where `j' : J` is such that for any `x : X`, there is a map `j x ⟶ j'`
  let j' := IsCardinalFiltered.max j hX
  let y' (x : X) : (p.diag.obj j').obj :=
    p.diag.map (IsCardinalFiltered.toMax j hX x) (y x)
  have hy' (x : X) : p.ι.app j' (y' x) = SetCardinalLT.singleton κ₁ x := by
    rw [← hy, ← p.w (IsCardinalFiltered.toMax j hX x)]
    rfl
  refine ⟨Set.range (p.ι.app j'), (hp j').of_surjective _
    (Set.rangeFactorization_surjective (f := p.ι.app j')), fun ⟨B, hB⟩ ↦ ?_⟩
  let j'' := IsCardinalFiltered.max (fun b ↦ y' b.val) hB
  refine ⟨_, ⟨j'', rfl⟩, fun b hb ↦ ?_⟩
  have : y' b ≤ j'' := (leOfHom (IsCardinalFiltered.toMax (fun b ↦ y' b.val) hB ⟨b, hb⟩) :)
  refine (p.ι.app j').hom.hom.monotone this ?_
  convert Set.mem_singleton b
  exact Subtype.ext_iff.1 (hy' b)

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
⊢ IsColimit ((coyoneda.obj (op X)).mapCocone c)

Tactic:
refine Types.FilteredColimit.isColimitOf' _ _ (fun f ↦ ?_) (fun j f g h ↦ ?_)

Goal state after:
case refine_1
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : ((coyoneda.obj (op X)).mapCocone c).pt
⊢ ∃ i xi, f = (hom (((coyoneda.obj (op X)).mapCocone c).ι.app i)) xi

case refine_2
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : (fun X ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)
h : (hom (((coyoneda.obj (op X)).mapCocone c).ι.app j)) f = (hom (((coyoneda.obj (op X)).mapCocone c).ι.app j)) g
⊢ ∃ k f_1, (hom ((F ⋙ coyoneda.obj (op X)).map f_1)) f = (hom ((F ⋙ coyoneda.obj (op X)).map f_1)) g
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c✝ : Cocone F
hc : IsColimit c✝
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c✝.ι.app j = g ≫ c✝.ι.app j
k : ToType X → J
a : (x : ToType X) → j ⟶ k x
hk : ∀ (x : ToType X), (hom (F.map (a x))) ((hom f) x) = (hom (F.map (a x))) ((hom g) x)
l : J
b : j ⟶ l
c : (x : ToType X) → k x ⟶ l
hl : ∀ (x : ToType X), a x ≫ c x = b
⊢ f ≫ F.map b = g ≫ F.map b

Tactic:
by ext x; simp [← hl x, hk]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
x✝ : IsCardinalPresentable X κ
this :
  ∀ (J : Type u) [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J (coyoneda.obj (op X))
A : Set X
hA : HasCardinalLT (↑A) κ
f : (HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨A, hA⟩
hf : (hom (((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).ι.app ⟨A, hA⟩)) f = 𝟙 X
⊢ A = Set.univ

Tactic:
by
    ext x
    have := congr_hom hf x
    dsimp at this
    rw [← this]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X Y✝ : C
f : Y✝ ⟶ X
S : Presieve X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (Sigma.desc π)
Z' : α → C := fun a ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y✝ := fun a ↦ pullback.fst f (π a)
Y : C
a : α
⊢ pullback.snd f (π a) ≫ π a = π' a ≫ f

Tactic:
CategoryTheory.Limits.pullback.condition

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X Y✝ : C
f : Y✝ ⟶ X
S : Presieve X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (Sigma.desc π)
Z' : α → C := fun a ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y✝ := fun a ↦ pullback.fst f (π a)
Y : C
a : α
⊢ pullback.snd f (π a) ≫ π a = pullback.snd f (π a) ≫ π a
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: case mp.of
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = Presieve.ofArrows Y' π
right✝ : EffectiveEpiFamily Y' π
a' : a
⊢ (Sieve.generate T).arrows (π a')

Tactic:
obtain ⟨rfl, _⟩ := h'

Goal state after:
case mp.of
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
right✝ : EffectiveEpiFamily Y' π
a' : a
⊢ (Sieve.generate (Presieve.ofArrows Y' π)).arrows (π a')
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case refine_1.refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
Z : Fin n → C := fun i ↦ unop (K.obj { as := i })
this✝ : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (∐ Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun i ↦ op (Z i) := Discrete.natIsoFunctor
⊢ IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)

Tactic:
apply hF
      refine ⟨Empty, inferInstance, Empty.elim, IsEmpty.elim inferInstance, rfl, ⟨default,?_, ?_⟩⟩
      · ext b
        cases b
      · simp only [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
x✝ : ∃ Y π, EffectiveEpi π ∧ S.arrows π
Y : C
π : Y ⟶ X
H₁ : EffectiveEpi π
H₂ : S.arrows π
⊢ EffectiveEpi (F.map π)

Tactic:
exact F.map_effectiveEpi _

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (regularTopology C) f → Presheaf.IsLocallySurjective (coherentTopology C) f

Tactic:
refine Presheaf.isLocallySurjective_of_le (J := regularTopology C) ?_ _
    rw [← extensive_regular_generate_coherent]
    exact (Coverage.gi _).gc.monotone_l le_sup_right

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
obj : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)
hom_comp :
  ∀ (i₁ i₂ i₃ : ι),
    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯ ≫
        pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
      pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯
Y : C
q : Y ⟶ S
i₁ i₂ i₃ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
f₃ : Y ⟶ X i₃
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hf₃ : f₃ ≫ f i₃ = q
⊢ pullHom' hom q f₁ f₂ ⋯ ⋯ ≫ pullHom' hom q f₂ f₃ ⋯ ⋯ = pullHom' hom q f₁ f₃ ⋯ ⋯

Tactic:
obtain ⟨φ, _, _, _⟩ := (sq₃ i₁ i₂ i₃).exists_lift f₁ f₂ f₃ q hf₁ hf₂ hf₃
  rw [← pullHom_pullHom'_assoc hom φ (sq₃ i₁ i₂ i₃).p _ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ _ _,
    ← pullHom_pullHom' hom φ (sq₃ i₁ i₂ i₃).p _ (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ _ _,
    ← pullHom_pullHom' hom φ (sq₃ i₁ i₂ i₃).p _ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ _ _]
  dsimp [pullHom]
  simp [← Functor.map_comp_assoc, hom_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
h₁ : p ≫ (sq i₁ i₂).p₁ = f₁
h₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ f₁ ≫ f i₁ = ?m.156

Tactic:
hf₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
h₁ : p ≫ (sq i₁ i₂).p₁ = f₁
h₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ q = ?m.156
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
⊢ ∀ (hf₁ : f₁ ≫ f' j₁ = q) (hf₂ : f₂ ≫ f' j₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map (D.iso (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' j₁) ⋯ ⋯).hom ≫
        ((pullFunctor F w').obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map (D.iso (p' j₂ ≫ f (α j₂)) (p' j₂) (p'' j₂) ⋯ ⋯).hom

Tactic:
hf₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
⊢ ∀ (hf₂ : f₂ ≫ f' j₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map (D.iso (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' j₁) ⋯ ⋯).hom ≫
        ((pullFunctor F w').obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map (D.iso (p' j₂ ≫ f (α j₂)) (p' j₂) (p'' j₂) ⋯ ⋯).hom
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
⊢ ∀ ⦃Y : C⦄ (q : Y ⟶ S') ⦃i₁ i₂ : ι'⦄ (f₁ : Y ⟶ X' i₁) (f₂ : Y ⟶ X' i₂) (hf₁ : f₁ ≫ f' i₁ = q) (hf₂ : f₂ ≫ f' i₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map (D.iso (p' i₁ ≫ f (α i₁)) (p' i₁) (p'' i₁) ⋯ ⋯).hom ≫
        ((pullFunctor F w').obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map (D.iso (p' i₂ ≫ f (α i₂)) (p' i₂) (p'' i₂) ⋯ ⋯).hom

Tactic:
intro Y q j₁ j₂ f₁ f₂ hf₁ hf₂

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ (F.map f₁.op.toLoc).toFunctor.map (D.iso (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' j₁) ⋯ ⋯).hom ≫
      ((pullFunctor F w').obj D).hom q f₁ f₂ ⋯ ⋯ =
    ((pullFunctor F w).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
      (F.map f₂.op.toLoc).toFunctor.map (D.iso (p' j₂ ≫ f (α j₂)) (p' j₂) (p'' j₂) ⋯ ⋯).hom