mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f : X ⟶ Y
⊢ sourceLocalClosure K P f ↔ ∃ R ∈ K.coverings X, ∀ (U : C) (g : U ⟶ X), R g → P (g ≫ f)

Tactic:
by
  refine ⟨?_, ?_⟩
  · intro h
    induction h with
    | of f hf => exact ⟨.singleton (𝟙 _), K.mem_coverings_of_isIso _, fun U g ⟨⟩ ↦ by simpa⟩
    | of_iso f g e hf h =>
      obtain ⟨R, hR, h⟩ := h
      rw [K.mem_iff_exists_zeroHypercover] at hR
      obtain ⟨E, rfl⟩ := hR
      refine ⟨_, (E.pushforward e.hom.left (K.mem_coverings_of_isIso _)).mem₀, ?_⟩
      intro U v ⟨i⟩
      dsimp
      simp only [Category.assoc, Arrow.w_mk_right, Arrow.mk_left, Arrow.mk_right, Arrow.mk_hom]
      rw [← Category.assoc, P.cancel_right_of_respectsIso]
      exact h _ _ ⟨i⟩
    | comp f hf R hR g hg ih =>
      obtain ⟨S, hS, h⟩ := ih
      rw [K.mem_iff_exists_zeroHypercover] at hS hR
      obtain ⟨E, rfl⟩ := hS
      obtain ⟨F, rfl⟩ := hR
      refine ⟨(E.pullback₁ g).presieve₀, (E.pullback₁ g).mem₀, ?_⟩
      intro U v ⟨i⟩
      dsimp
      rw [pullback.condition_assoc]
      refine RespectsLeft.precomp (Q := K.morphismProperty) _ ?_ _ ?_
      · obtain ⟨j⟩ := hg
        exact (F.pullback₂ (E.f i)).morphismProperty j
      · exact h _ _ ⟨i⟩
    | of_presieve f R hR h ih =>
      rw [K.mem_iff_exists_zeroHypercover] at hR
      obtain ⟨E, rfl⟩ := hR
      choose S hS h' using fun i : E.I₀ ↦ ih _ _ ⟨i⟩
      simp_rw [K.mem_iff_exists_zeroHypercover] at hS
      choose F hF using hS
      refine ⟨_, (E.bind F).mem₀, fun U g ⟨j⟩ ↦ ?_⟩
      dsimp
      rw [Category.assoc]
      exact h' _ _ _ (by simp [hF])
  · intro ⟨R, hR, h⟩
    exact .of_presieve _ _ hR (by grind)

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
⊢ ∑ j,
      eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            ((biproduct.π (fun b ↦ s (g b)) j ≫ biproduct.ι (fun b ↦ s (g b)) j) ≫ w) ≫
              biproduct.π (fun b ↦ s (h b)) c =
    ∑ x,
      eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫ biproduct.π (fun b ↦ s (g b)) ↑x ≫ biproduct.ι (fun a ↦ s (g a)) ↑x ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c

Tactic:
apply Finset.sum_congr_set

Goal state after:
case w
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
⊢ ∀ (x : β) (hx : x ∈ g ⁻¹' {h c}),
    eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            ((biproduct.π (fun b ↦ s (g b)) x ≫ biproduct.ι (fun b ↦ s (g b)) x) ≫ w) ≫
              biproduct.π (fun b ↦ s (h b)) c =
      eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            biproduct.π (fun b ↦ s (g b)) ↑⟨x, hx⟩ ≫
              biproduct.ι (fun a ↦ s (g a)) ↑⟨x, hx⟩ ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c

case w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
⊢ ∀ x ∉ g ⁻¹' {h c},
    eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            ((biproduct.π (fun b ↦ s (g b)) x ≫ biproduct.ι (fun b ↦ s (g b)) x) ≫ w) ≫
              biproduct.π (fun b ↦ s (h b)) c =
      0
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a ↦ s (f a)) ≅ ⨁ fun b ↦ s (g b)
⊢ ∃ e, ∀ (a : α), g (e a) = f a

Tactic:
classical
  refine ⟨Equiv.ofPreimageEquiv ?_, fun a => Equiv.ofPreimageEquiv_map _ _⟩
  intro c
  apply Nonempty.some
  apply Cardinal.eq.1
  cases nonempty_fintype α; cases nonempty_fintype β
  simp only [Cardinal.mk_fintype, Nat.cast_inj]
  exact
    Matrix.square_of_invertible (o.matrixDecomposition i.inv c) (o.matrixDecomposition i.hom c)
      (by
        rw [← o.matrixDecomposition_comp]
        simp)
      (by
        rw [← o.matrixDecomposition_comp]
        simp)

Goal state after:
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:
pp: X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ (m₂ a e₁) (m₂ e₁ b) = m₂ a b

Tactic:
simp only [distrib, h₁.left_id, h₁.right_id]

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
A : Type u
inst✝¹ : SmallCategory A
inst✝ : IsCardinalFiltered A κ
⊢ PreservesColimitsOfShape A (forget (CardinalDirectedPoset κ))

Tactic:
by
  have := isFiltered_of_isCardinalFiltered A κ
  change PreservesColimitsOfShape A (CardinalDirectedPoset.ι ⋙ forget _)
  infer_instance

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: α : PartOrdEmb
P : Set ↑α → Prop
inst✝¹ : IsDirectedOrder (Subtype P)
inst✝ : Nonempty (Subtype P)
hP : ∀ (a : ↑α), ∃ J, P J ∧ a ∈ J
⊢ IsColimit ((forget PartOrdEmb).mapCocone (coconeOfPredicateSet P))

Tactic:
refine Types.FilteredColimit.isColimitOf' _ _ (fun a ↦ ?_)
      (fun J x y h ↦ ⟨J, 𝟙 _, Subtype.ext h⟩)

Goal state after:
α : PartOrdEmb
P : Set ↑α → Prop
inst✝¹ : IsDirectedOrder (Subtype P)
inst✝ : Nonempty (Subtype P)
hP : ∀ (a : ↑α), ∃ J, P J ∧ a ∈ J
a : ((forget PartOrdEmb).mapCocone (coconeOfPredicateSet P)).pt
⊢ ∃ i xi, a = (ConcreteCategory.hom (((forget PartOrdEmb).mapCocone (coconeOfPredicateSet P)).ι.app i)) xi
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 κ₁
hp : ∀ (j : J), HasCardinalLT (↑(p.diag.obj j).obj) κ₂
j : X → J
y : (x : X) → ToType (p.diag.obj (j x))
hy : ∀ (x : X), (ConcreteCategory.hom (p.ι.app (j x))) (y x) = SetCardinalLT.singleton κ₁ x
j' : J := IsCardinalFiltered.max j hX
y' : X → ↑(p.diag.obj j').obj := fun x ↦ (ConcreteCategory.hom (p.diag.map (IsCardinalFiltered.toMax j hX x))) (y x)
hy' : ∀ (x : X), (ConcreteCategory.hom (p.ι.app j')) (y' x) = SetCardinalLT.singleton κ₁ x
⊢ ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y

Tactic:
refine ⟨Set.range (p.ι.app j'), (hp j').of_surjective _
    (Set.rangeFactorization_surjective (f := p.ι.app j')), fun ⟨B, hB⟩ ↦ ?_⟩

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) κ₂
j : X → J
y : (x : X) → ToType (p.diag.obj (j x))
hy : ∀ (x : X), (ConcreteCategory.hom (p.ι.app (j x))) (y x) = SetCardinalLT.singleton κ₁ x
j' : J := IsCardinalFiltered.max j hX
y' : X → ↑(p.diag.obj j').obj := fun x ↦ (ConcreteCategory.hom (p.diag.map (IsCardinalFiltered.toMax j hX x))) (y x)
hy' : ∀ (x : X), (ConcreteCategory.hom (p.ι.app j')) (y' x) = SetCardinalLT.singleton κ₁ x
x✝ : SetCardinalLT κ₁ X
B : Set X
hB : HasCardinalLT (↑B) κ₁
⊢ ∃ y ∈ Set.range ⇑(ConcreteCategory.hom (p.ι.app j')), ⟨B, hB⟩ ≤ y
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: case succ
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : ¬IsMax j
hj' : HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂
hκ₂ : κ₂.IsRegular
x✝ : ↑(Y (transfiniteIterate (φ Y m) j A) hj')
C : SetCardinalLT κ₁ ↑(transfiniteIterate (φ Y m) j A)
hC : C ∈ Y (transfiniteIterate (φ Y m) j A) hj'
⊢ HasCardinalLT (↑(Subtype.val '' ↑↑⟨C, hC⟩)) κ₂

Tactic:
refine (C.prop.of_le h₀.le).of_injective (fun ⟨c, hc⟩ ↦ ?_)
      (fun c₁ c₂ hc ↦ ?_)

Goal state after:
case succ.refine_1
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : ¬IsMax j
hj' : HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂
hκ₂ : κ₂.IsRegular
x✝¹ : ↑(Y (transfiniteIterate (φ Y m) j A) hj')
C : SetCardinalLT κ₁ ↑(transfiniteIterate (φ Y m) j A)
hC : C ∈ Y (transfiniteIterate (φ Y m) j A) hj'
x✝ : ↑(Subtype.val '' ↑↑⟨C, hC⟩)
c : X
hc : c ∈ Subtype.val '' ↑↑⟨C, hC⟩
⊢ ↑↑C

case succ.refine_2
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : ¬IsMax j
hj' : HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂
hκ₂ : κ₂.IsRegular
x✝ : ↑(Y (transfiniteIterate (φ Y m) j A) hj')
C : SetCardinalLT κ₁ ↑(transfiniteIterate (φ Y m) j A)
hC : C ∈ Y (transfiniteIterate (φ Y m) j A) hj'
c₁ c₂ : ↑(Subtype.val '' ↑↑⟨C, hC⟩)
hc :
  (fun x ↦
        match x with
        | ⟨c, hc⟩ => ?succ.refine_1)
      c₁ =
    (fun x ↦
        match x with
        | ⟨c, hc⟩ => ?succ.refine_1)
      c₂
⊢ c₁ = c₂
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
inst✝ : PartialOrder X
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
hm : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : SetCardinalLT κ₁ ↑B) (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC
A : Set X
hA : HasCardinalLT (↑A) κ₂
K : Type w
j : κ₁.ord.ToType
f : K → ↑(transfiniteIterate (φ Y m) j A)
hK : HasCardinalLT K κ₁
x : X
hx : x ∈ φ₀ Y m (transfiniteIterate (φ Y m) j A) ⋯
hx' : ∀ (t : K), ↑(f t) ≤ ↑⟨x, hx⟩
this : NoMaxOrder κ₁.ord.ToType
⊢ x ∈ transfiniteIterate (φ Y m) (Order.succ j) A

Tactic:
rwa [transfiniteIterate_succ _ _ _ (not_isMax j),
    φ_eq _ _ _ (hasCardinalLT_transfiniteIterate_φ h₀ Y hY m A hA _)]

Goal state after:
Module: Mathlib.CategoryTheory.RepresentedBy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
Y : C
e : Y ≅ X
⊢ F.IsRepresentedBy ((ConcreteCategory.hom (F.map e.hom.op)) x)

Tactic:
rw [iff_exists_representableBy]
  use h.representableBy.ofIsoObj e
  simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
W : C
⊢ Presieve.IsSheaf (coherentTopology C) (yoneda.obj W)

Tactic:
rw [isSheaf_coherent]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
W : C
⊢ ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows X π)
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (Presieve.ofArrows
        (fun x ↦
          match x with
          | ⟨a, b⟩ => Y_n a b)
        fun x ↦
        match x with
        | ⟨a, b⟩ => π_n a b ≫ π a) ∈
    (coherentTopology C) X
⊢ (Presieve.ofArrows (fun c ↦ Y_n c.fst c.snd) fun c ↦ π_n c.fst c.snd ≫ π c.fst).EffectiveEpimorphic

Tactic:
change Nonempty _

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (Presieve.ofArrows
        (fun x ↦
          match x with
          | ⟨a, b⟩ => Y_n a b)
        fun x ↦
        match x with
        | ⟨a, b⟩ => π_n a b ≫ π a) ∈
    (coherentTopology C) X
⊢ Nonempty
    (Limits.IsColimit
      (Sieve.generate (Presieve.ofArrows (fun c ↦ Y_n c.fst c.snd) fun c ↦ π_n c.fst c.snd ≫ π c.fst)).arrows.cocone)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
h₂ : Sieve.generate (Presieve.ofArrows ?m.50 ?m.51) ∈ (regularTopology C) X
⊢ (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π).EffectiveEpimorphic

Tactic:
change Nonempty _

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
h₂ : Sieve.generate (Presieve.ofArrows ?m.50 ?m.51) ∈ (regularTopology C) X
⊢ Nonempty (IsColimit (Sieve.generate (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π)).arrows.cocone)
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits

Goal state before:
pp: A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
⊢ PreservesFiniteProducts (G ⋙ sheafToPresheaf (extensiveTopology C) A).flip

Tactic:
have : ∀ (i : J), PreservesFiniteProducts ((G ⋙ sheafToPresheaf _ A).obj i) := fun i ↦ by
    rw [← Presheaf.isSheaf_iff_preservesFiniteProducts]
    exact (G.obj i).property

Goal state after:
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
this : ∀ (i : J), PreservesFiniteProducts ((G ⋙ sheafToPresheaf (extensiveTopology C) A).obj i)
⊢ PreservesFiniteProducts (G ⋙ sheafToPresheaf (extensiveTopology C) A).flip
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP : Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯))
hc : IsLimit c
⊢ ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y

Tactic:
rw [Function.bijective_iff_existsUnique] at hP

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
hc : IsLimit c
⊢ ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ S ∈ (extensiveTopology C) X

Tactic:
apply (extensiveCoverage C).mem_toGrothendieck_sieves_of_superset (R := Presieve.ofArrows Y π)

Goal state after:
case mpr.h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ≤ S.arrows

case mpr.hR
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ∈ (extensiveCoverage C).coverings X
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP : Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯))
⊢ ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y

Tactic:
rw [Function.bijective_iff_existsUnique] at hP

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀
    (b :
      (fun X ↦ X)
        ↑{x |
            (ConcreteCategory.hom (P.map (pullback.fst π π).op)) x =
              (ConcreteCategory.hom (P.map (pullback.snd π π).op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)) a = b
⊢ ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
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))
n : ℕ
⊢ EffectiveEpi ((preimageDiagram hF X y).map (homOfLE ⋯).op)

Tactic:
by simpa [preimageDiagram] using (preimageStruct hF X y).effectiveEpi n

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
inst✝³ : HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R
S : C
M N : ↑(F.obj { as := op S })
X : Over S
R : Presieve X
hR : Presieve.map (Over.forget S) R ∈ J.coverings X.left
R' : Sieve X.left
hR' : (Sieve.overEquiv X).symm R' = Sieve.generate R
⊢ Presieve.IsSheafFor (F.presheafHom M N) R

Tactic:
rw [Presieve.isSheafFor_iff_generate]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst✝³ : HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R
S : C
M N : ↑(F.obj { as := op S })
X : Over S
R : Presieve X
hR : Presieve.map (Over.forget S) R ∈ J.coverings X.left
R' : Sieve X.left
hR' : (Sieve.overEquiv X).symm R' = Sieve.generate R
⊢ Presieve.IsSheafFor (F.presheafHom M N) (Sieve.generate R).arrows
Module: Mathlib.CategoryTheory.Sites.Point.Monoidal

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ P₃ : Cᵒᵖ ⥤ A
X : C
x : Φ.fiber.obj X
| ((Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x P₂) ⊗ₘ Φ.toPresheafFiber X x P₃) ≫
    (α_ (Φ.presheafFiber.obj P₁) (Φ.presheafFiber.obj P₂) (Φ.presheafFiber.obj P₃)).hom

Tactic:
associator_naturality

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ P₃ : Cᵒᵖ ⥤ A
X : C
x : Φ.fiber.obj X
| (α_ (P₁.obj (Opposite.op X)) (P₂.obj (Opposite.op X)) (P₃.obj (Opposite.op X))).hom ≫
    (Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x P₂ ⊗ₘ Φ.toPresheafFiber X x P₃)
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
F : Cᵒᵖ ⥤ Type w
h : Presieve.IsSheaf J F
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor F R

Tactic:
rw [Presieve.isSheafFor_iff_generate]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
F : Cᵒᵖ ⥤ Type w
h : Presieve.IsSheaf J F
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor F (Sieve.generate R).arrows
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor (Functor.closedSieves K.toGrothendieck).toFunctor R

Tactic:
rw [Presieve.isSheafFor_iff_generate]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor (Functor.closedSieves K.toGrothendieck).toFunctor (Sieve.generate R).arrows