mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j✝ : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j✝ ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
j : J
hj : D.P j
hl₁ hl₂ : (D₄ D φ).W (φ ⟨j, hj⟩)
⊢ φ ⟨j, hj⟩ = φ ⟨j, hj⟩

Tactic:
rfl

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

Goal state before:
pp: case inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
hm₁ : (D₄ D φ).IsTerminal m₁ := Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
lift_eq : ∀ (j : J) (hj : D.P j), hm₁.lift ⋯ = φ ⟨j, hj⟩
i✝ : Unit
hj : (D₄ D φ).IsTerminal m₁
⊢ m₁ = m₁

Tactic:
rfl

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

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
⊢ (functor J κ).Final

Tactic:
have := isCardinalFiltered J κ hJ
  have := isFiltered_of_isCardinalFiltered J κ
  have := isFiltered_of_isCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
  rw [Functor.final_iff_of_isFiltered]
  refine ⟨fun j ↦ ⟨.single j, ⟨𝟙 _⟩⟩, fun {j D} (f₁ f₂ : j ⟶ D.top) ↦ ?_⟩
  obtain ⟨m₀, t, hm₀⟩ := hJ D.top
  obtain ⟨m₁, u, hu⟩ : ∃ (m₁ : J) (u : m₀ ⟶ m₁), f₁ ≫ t ≫ u = f₂ ≫ t ≫ u :=
    ⟨_, IsFiltered.coeqHom (f₁ ≫ t) (f₂ ≫ t),
      by simpa using IsFiltered.coeq_condition (f₁ ≫ t) (f₂ ≫ t)⟩
  have h₁ : ¬ (D.P m₁) := fun h₁ ↦ hm₀.false (u ≫ D.isTerminal.lift h₁)
  let φ (x : Subtype D.P) : x.1 ⟶ m₁ := D.isTerminal.lift x.2 ≫ t ≫ u
  have h₂ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f) :
      f = φ ⟨_, hj⟩ := by
    obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨⟩⟩) := hf
    · exact (h₁ (D.tgt hf)).elim
    · exact (h₁ hj).elim
    · rfl
  have h₃ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f) : f = 𝟙 _ := by
    obtain ((hf | ⟨⟨⟩⟩) | hf) := hf
    · exact (h₁ (D.src hf)).elim
    · rfl
    · rw [MorphismProperty.ofHoms_iff] at hf
      obtain ⟨⟨j, hj⟩, hf⟩ := hf
      obtain rfl : m₁ = j := congr_arg Arrow.leftFunc.obj hf
      exact (h₁ hj).elim
  let hm₁ : (D₄ D φ).IsTerminal m₁ :=
    .ofExistsUnique (Or.inl (Or.inr ⟨⟨⟩⟩)) (by
        rintro j (hj | ⟨⟨⟨⟩⟩⟩)
        · exact ⟨φ ⟨_, hj⟩, Or.inr ⟨_⟩⟩
        · exact ⟨𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩)⟩) (by
        rintro j (hj | ⟨⟨⟨⟩⟩⟩) l₁ l₂ hl₁ hl₂
        · obtain rfl := h₂ hj hl₁
          obtain rfl := h₂ hj hl₂
          rfl
        · rw [h₃ hl₁, h₃ hl₂]) (by
      rintro j k f ((hf | ⟨⟨⟩⟩) | ⟨⟨j, hj⟩⟩)
      · exact ⟨φ ⟨_, D.src hf⟩, φ ⟨_, D.tgt hf⟩,
          Or.inr ⟨_⟩, Or.inr ⟨_⟩, D.isTerminal.comm_assoc _ hf _⟩
      · exact ⟨𝟙 _, 𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩), Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩
      · exact ⟨φ ⟨_, hj⟩, 𝟙 _, Or.inr ⟨_⟩, Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩)
  have lift_eq (j : J) (hj : D.P j) : hm₁.lift (Or.inl hj) = φ ⟨_, hj⟩ :=
    hm₁.uniq _ (Or.inr ⟨_⟩)
  let D₄' : DiagramWithUniqueTerminal J κ :=
    { toDiagram := D₄ D φ
      top := m₁
      isTerminal := hm₁
      uniq_terminal j hj := by
        obtain (hj' | ⟨⟨⟩⟩) := hj.prop
        · exact hm₀.elim (u ≫ hj.lift (Or.inr ⟨⟨⟩⟩) ≫ D.isTerminal.lift hj')
        · rfl }
  exact ⟨D₄', homOfLE ⟨le_sup_left.trans le_sup_left, le_sup_left⟩,
    by simpa [functorMap, D₄', lift_eq _ D.isTerminal.prop, φ]⟩

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

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
⊢ S ∈ (regularTopology C) X → ∃ Y π, EffectiveEpi π ∧ S.arrows π

Tactic:
intro h
    induction h with
    | of Y T hS =>
      rcases hS with ⟨Y', π, h'⟩
      refine ⟨Y', π, h'.2, ?_⟩
      rcases h' with ⟨rfl, _⟩
      exact ⟨Y', 𝟙 Y', π, Presieve.ofArrows.mk (), (by simp)⟩
    | top Y => exact ⟨Y, (𝟙 Y), inferInstance, by simp only [Sieve.top_apply]⟩
    | transitive Y R S _ _ a b =>
      rcases a with ⟨Y₁, π, ⟨h₁, h₂⟩⟩
      choose Y' π' _ H using b h₂
      exact ⟨Y', π' ≫ π, inferInstance, (by simpa using H)⟩

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a ↦ Exists.choose ⋯
ht : IsLimit (Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone :=
  (Types.productLimitCone fun a ↦ F.obj (op (Y a))).isLimit
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as))))
a : α
⊢ (ConcreteCategory.hom
        (((Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone.π.app { as := a } ≫
            (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as)))).hom.app { as := a }) ≫
          f.app (op (Y a))))
      y =
    (ConcreteCategory.hom (f.app (op (Y a)))) (Exists.choose ⋯)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
X : C
y : ToType ((F.obj (op 0)).obj.obj (op X))
hh : EffectiveEpi (limit.π (preimageDiagram hF X y) (op 0))
⊢ (ConcreteCategory.hom
        (((coherentTopology C).yonedaEquiv.symm ((preimageStruct hF X y).x 0)).hom.app
          (op (limit (preimageDiagram hF X y)))))
      (limit.π (preimageDiagram hF X y) (op 0)) =
    (ConcreteCategory.hom ((F.obj (op 0)).obj.map (op (limit.π (preimageDiagram hF X y) (op 0))))) y

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this✝ :
  (Sieve.overEquiv (Over.mk (𝟙 (X i)))).symm (Sieve.pullback (f i) (Sieve.ofArrows X' f')) ∈
    (J.over (X i)) (Over.mk (𝟙 (X i)))
Z : Over (X i)
Y : C
j : ι'
p : Z.left ⟶ X' j
ψ : D₁ ⟶ D₂
hp : p ≫ f' j = Over.Hom.left (Over.homMk Z.hom ⋯) ≫ f i
this : Over.Hom.left (Over.homMk Z.hom ⋯) = Z.hom
⊢ (p ≫ p' j) ≫ f (α j) = Z.hom ≫ f i

Tactic:
grind

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)
obj 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)
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
hp₁ : ⋯.lift f₁ f₂ ⋯ ≫ (sq i₁ i₂).p₁ = f₁
hp₂ : ⋯.lift f₁ f₂ ⋯ ≫ (sq i₁ i₂).p₂ = f₂
⊢ pullHom' hom q f₁ f₂ hf₁ hf₂ = pullHom (hom i₁ i₂) (⋯.lift f₁ f₂ ⋯) f₁ f₂ ⋯ ⋯

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
⊢ mor w φ q a fac =
    D₁.hom (q ≫ f i) q (a ≫ p' j) ⋯ ⋯ ≫
      pullHom (φ.hom j) a (a ≫ p' j) (a ≫ p' j) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a ≫ p' j) q ⋯ ⋯

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
Z' : C
r : Z' ⟶ Z
r' : Z' ⟶ X i
a' : Z' ⟶ X' j
hr' : r ≫ q = r'
ha' : r ≫ a = a'
this :
  (F.mapComp' a.op.toLoc r.op.toLoc a'.op.toLoc ⋯).hom.toNatTrans.app
        ((F.map (p' j).op.toLoc).toFunctor.obj (D₁.obj (α j))) ≫
      (F.map r.op.toLoc).toFunctor.map ((F.map a.op.toLoc).toFunctor.map (φ.hom j)) ≫
        (F.mapComp' a.op.toLoc r.op.toLoc a'.op.toLoc ⋯).inv.toNatTrans.app
          ((F.map (p' j).op.toLoc).toFunctor.obj (D₂.obj (α j))) =
    (F.map a'.op.toLoc).toFunctor.map (φ.hom j)
⊢ a.op.toLoc ≫ r.op.toLoc = a'.op.toLoc

Tactic:
grind

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
Z' : C
r : Z' ⟶ Z
r' : Z' ⟶ X i
a' : Z' ⟶ X' j
hr' : r ≫ q = r'
ha' : r ≫ a = a'
this :
  (F.mapComp' a.op.toLoc r.op.toLoc a'.op.toLoc ⋯).hom.toNatTrans.app
        ((F.map (p' j).op.toLoc).toFunctor.obj (D₁.obj (α j))) ≫
      (F.map r.op.toLoc).toFunctor.map ((F.map a.op.toLoc).toFunctor.map (φ.hom j)) ≫
        (F.mapComp' a.op.toLoc r.op.toLoc a'.op.toLoc ⋯).inv.toNatTrans.app
          ((F.map (p' j).op.toLoc).toFunctor.obj (D₂.obj (α j))) =
    (F.map a'.op.toLoc).toFunctor.map (φ.hom j)
⊢ (p' j).op.toLoc ≫ a'.op.toLoc = ((p' j).op.toLoc ≫ a.op.toLoc) ≫ r.op.toLoc

Tactic:
grind

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
Z' : C
r : Z' ⟶ Z
r' : Z' ⟶ X i
a' : Z' ⟶ X' j
hr' : r ≫ q = r'
ha' : r ≫ a = a'
this :
  (F.mapComp' a.op.toLoc r.op.toLoc a'.op.toLoc ⋯).hom.toNatTrans.app
        ((F.map (p' j).op.toLoc).toFunctor.obj (D₁.obj (α j))) ≫
      (F.map r.op.toLoc).toFunctor.map ((F.map a.op.toLoc).toFunctor.map (φ.hom j)) ≫
        (F.mapComp' a.op.toLoc r.op.toLoc a'.op.toLoc ⋯).inv.toNatTrans.app
          ((F.map (p' j).op.toLoc).toFunctor.obj (D₂.obj (α j))) =
    (F.map a'.op.toLoc).toFunctor.map (φ.hom j)
⊢ ((p' j).op.toLoc ≫ a.op.toLoc) ≫ r.op.toLoc = ((p' j).op.toLoc ≫ a.op.toLoc) ≫ r.op.toLoc

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
F : Cᵒᵖ ⥤ Type u_3
⊢ Nonempty (IsLimit (E.saturate.multifork F)) ↔ Presieve.IsSheafFor F E.presieve₀

Tactic:
rw [Multifork.isLimit_types_iff, Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible,
    ← Function.Bijective.of_comp_iff' (E.sectionsSaturateEquiv F).symm.bijective]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
F : Cᵒᵖ ⥤ Type u_3
⊢ Function.Bijective (E.saturate.multifork F).toSections ↔
    Function.Bijective (⇑(E.sectionsSaturateEquiv F).symm ∘ Presieve.Arrows.toCompatible F E.f)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
F : Cᵒᵖ ⥤ Type u_3
⊢ Function.Bijective (E.saturate.multifork F).toSections ↔
    Function.Bijective (⇑(E.sectionsSaturateEquiv F).symm ∘ Presieve.Arrows.toCompatible F E.f)

Tactic:
rfl

Goal state after:
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
D : F.DescentData f
M : ↑(F.obj { as := op S })
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 i₁).op.toLoc ≫ f₁.op.toLoc = q.op.toLoc

Tactic:
grind

Goal state after:
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
D : F.DescentData f
M : ↑(F.obj { as := op S })
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 i₂).op.toLoc ≫ f₂.op.toLoc = q.op.toLoc

Tactic:
grind

Goal state after:
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
D : F.DescentData f
M : ↑(F.obj { as := op S })
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
hq : g ≫ q = q'
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ (f i₁).op.toLoc ≫ f₁.op.toLoc = q.op.toLoc

Tactic:
grind

Goal state after:
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
D : F.DescentData f
M : ↑(F.obj { as := op S })
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
hq : g ≫ q = q'
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ f₁.op.toLoc ≫ g.op.toLoc = gf₁.op.toLoc

Tactic:
grind

Goal state after:
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
D : F.DescentData f
M : ↑(F.obj { as := op S })
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
hq : g ≫ q = q'
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ (f i₁).op.toLoc ≫ gf₁.op.toLoc = q'.op.toLoc

Tactic:
grind

Goal state after:
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
D : F.DescentData f
M : ↑(F.obj { as := op S })
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
hq : g ≫ q = q'
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ (f i₂).op.toLoc ≫ f₂.op.toLoc = q.op.toLoc

Tactic:
grind

Goal state after:
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
D : F.DescentData f
M : ↑(F.obj { as := op S })
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
hq : g ≫ q = q'
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ f₂.op.toLoc ≫ g.op.toLoc = gf₂.op.toLoc

Tactic:
grind

Goal state after:
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
D : F.DescentData f
M : ↑(F.obj { as := op S })
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
hq : g ≫ q = q'
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ q.op.toLoc ≫ g.op.toLoc = q'.op.toLoc

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Sites.LocalSite

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : J.IsLocalSite
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P : Cᵒᵖ ⥤ A
X : C
x : (point J).fiber.obj X
⊢ P.map
      (↑((IsInitial.op (shrinkCoyoneda.{w, v, u}.obj (op (⊤_ C))).Elements
                  (Functor.Elements.isInitialOfCorepresentableBy (shrinkCoyonedaCorepresentableBy (op (⊤_ C))))).from
              (op ⟨X, x⟩)).unop).op =
    P.map (shrinkCoyonedaObjObjEquiv x).op

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ f₂.op.toLoc ≫ p.op.toLoc = (p ≫ f₂).op.toLoc

Tactic:
grind

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ g ≫ f' j = (p ≫ f₁) ≫ f i₁

Tactic:
grind

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ g ≫ f' j = (p ≫ f₂) ≫ f i₂

Tactic:
grind

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ (p ≫ f₁) ≫ f i₁ = p ≫ q

Tactic:
grind

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ (p ≫ f₂) ≫ f i₂ = p ≫ q

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X Y Z : C
f : Z ⟶ Y
g : Y ⟶ X
α : (presheafHom F G).obj (op X)
⊢ ((ConcreteCategory.hom ((presheafHom F G).map g.op)) α).app (op (Over.mk f)) = α.app (op (Over.mk (f ≫ g)))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
s : ↑(presheafHom F G).sections
X₁ X₂ : C
f : X₂ ⟶ X₁
⊢ F.map (op f) ≫ (↑s (op X₁)).app (op (Over.mk f)) = F.map f.op ≫ (↑s (op X₁)).app (op (Over.mk f))

Tactic:
rfl

Goal state after: