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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁶ : Category.{v_1, u_1} J✝
inst✝⁵ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝⁴ : SmallCategory J
inst✝³ : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝² : IsFiltered J
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)
k l : Total P
⊢ ∃ Z x x, True

Tactic:
by
    let a := IsFiltered.max k.1 l.1
    obtain ⟨a', f, hf⟩ := Total.exists_hom_of_hom (P := P) k.2 (IsFiltered.leftToMax k.1 l.1)
    obtain ⟨b', g, hg⟩ := Total.exists_hom_of_hom (P := P) l.2 (IsFiltered.rightToMax k.1 l.1)
    refine ⟨⟨a, IsFiltered.max a' b'⟩, ?_, ?_, trivial⟩
    · exact f ≫ { base := 𝟙 _, hom := (P _).diag.map (IsFiltered.leftToMax _ _) }
    · exact g ≫ { base := 𝟙 _, hom := (P _).diag.map (IsFiltered.rightToMax _ _) }

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : EssentiallySmall.{w, v', u'} J
inst✝ : IsCardinalFiltered J κ
X : C
p : (isCardinalPresentable C κ).ColimitOfShape J X
this : IsFiltered J
f : CostructuredArrow (isCardinalPresentable C κ).ι X
j : J
g₁ g₂ : f ⟶ p.toCostructuredArrow.obj j
k : J
a : j ⟶ k
h : g₁.left.hom ≫ p.diag.map a = g₂.left.hom ≫ p.diag.map a
⊢ ∃ c' t, g₁ ≫ p.toCostructuredArrow.map t = g₂ ≫ p.toCostructuredArrow.map t

Tactic:
exact ⟨k, a, by cat_disch⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsFinitelyAccessibleCategory C
X : C
⊢ IsFiltered (CostructuredArrow (ObjectProperty.isFinitelyPresentable C).ι X)

Tactic:
by
  rw [← CategoryTheory.isCardinalFiltered_aleph0_iff.{w},
    ObjectProperty.isFinitelyPresentable_eq_isCardinalPresentable]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
⊢ P X ≤ P.ind X

Tactic:
hX

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
hX : P X
⊢ P.ind X
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : P.ind g
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w✝¹ : SmallCategory J₁
w✝ : IsFiltered J₁
D₁ : J₁ ⥤ C
s₁ : (Functor.const J₁).obj X ⟶ D₁
t₁ : D₁ ⟶ (Functor.const J₁).obj Y
ht₁ : IsColimit { pt := Y, ι := t₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
⊢ ∃ W u_1 v, u_1 ≫ v = u ∧ P (p ≫ u_1)

Tactic:
obtain ⟨J₂, _, _, D₂, s₂, t₂, ht₂, h₂⟩ := hg

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w✝³ : SmallCategory J₁
w✝² : IsFiltered J₁
D₁ : J₁ ⥤ C
s₁ : (Functor.const J₁).obj X ⟶ D₁
t₁ : D₁ ⟶ (Functor.const J₁).obj Y
ht₁ : IsColimit { pt := Y, ι := t₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w✝¹ : SmallCategory J₂
w✝ : IsFiltered J₂
D₂ : J₂ ⥤ C
s₂ : (Functor.const J₂).obj Y ⟶ D₂
t₂ : D₂ ⟶ (Functor.const J₂).obj Z
ht₂ : IsColimit { pt := Z, ι := t₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
⊢ ∃ W u_1 v, u_1 ≫ v = u ∧ P (p ≫ u_1)
Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝³ : AddGroup A
inst✝² : HasShift C A
α : Type u_3
J : α → Type u_4
inst✝¹ : (i : α) → Category.{u_5, u_4} (J i)
inst✝ : P.IsStableUnderShift A
a : A
X : C
⊢ P.limitsClosure J X ≤ (P.limitsClosure J).shift a X

Tactic:
hX

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝³ : AddGroup A
inst✝² : HasShift C A
α : Type u_3
J : α → Type u_4
inst✝¹ : (i : α) → Category.{u_5, u_4} (J i)
inst✝ : P.IsStableUnderShift A
a : A
X : C
hX : P.limitsClosure J X
⊢ (P.limitsClosure J).shift a X
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
inst✝¹ : (i : I) → MonoidalCategory (C i)
inst✝ : (i : I) → SymmetricCategory (C i)
X Y : (i : I) → C i
⊢ (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)

Tactic:
by ext i; apply symmetry

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

Goal state before:
pp: case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : Fin n
a✝ : b ∈ Finset.univ
hb : b ≠ i
⊢ ∀ x ∈ Finset.univ,
    ((if h : i = b then if h' : h ▸ j = x then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = b then if h' : h ▸ j' = x then eqToHom ⋯ else 0 else 0) =
      0

Tactic:
intro x _

Goal state after:
case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : Fin n
a✝¹ : b ∈ Finset.univ
hb : b ≠ i
x : (f b).ι
a✝ : x ∈ Finset.univ
⊢ ((if h : i = b then if h' : h ▸ j = x then eqToHom ⋯ else 0 else 0) ≫
      if h : i' = b then if h' : h ▸ j' = x then eqToHom ⋯ else 0 else 0) =
    0
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : (f i).ι
a✝ : b ∈ Finset.univ
hb : b ≠ j
⊢ ((if h' : ⋯ ▸ j = b then eqToHom ⋯ else 0) ≫ if h : i' = i then if h' : h ▸ j' = b then eqToHom ⋯ else 0 else 0) = 0

Tactic:
dif_neg,

Goal state after:
case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : (f i).ι
a✝ : b ∈ Finset.univ
hb : b ≠ j
⊢ (0 ≫ if h : i' = i then if h' : h ▸ j' = b then eqToHom ⋯ else 0 else 0) = 0

case h₀.hnc
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : (f i).ι
a✝ : b ∈ Finset.univ
hb : b ≠ j
⊢ ¬⋯ ▸ j = b
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
s : Cocone F
j : J
x' y' : (F ⋙ forget PartOrdEmb).obj j
h :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) x') =
    (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) y')
⊢ (ConcreteCategory.hom (c.ι.app j)) x' = (ConcreteCategory.hom (c.ι.app j)) y'

Tactic:
obtain rfl := (s.ι.app j).injective
      (((ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) x').symm.trans h).trans
        (ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) y'))

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
s : Cocone F
j : J
x' : (F ⋙ forget PartOrdEmb).obj j
h :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) x') =
    (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) x')
⊢ (ConcreteCategory.hom (c.ι.app j)) x' = (ConcreteCategory.hom (c.ι.app j)) x'
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
prop_id : D.W (𝟙 e)
h₁ : ∀ ⦃j : J⦄, D.P j → ∃ lift, D.W lift
h₂ : ∀ ⦃j : J⦄, D.P j → ∀ (l₁ l₂ : j ⟶ e), D.W l₁ → D.W l₂ → l₁ = l₂
h₃ : ∀ ⦃i j : J⦄ (f : i ⟶ j), D.W f → ∃ li lj, D.W li ∧ D.W lj ∧ f ≫ lj = li
i✝ j✝ : J
x✝ : i✝ ⟶ j✝
hf : D.W x✝
⊢ x✝ ≫ ⋯.choose = ⋯.choose

Tactic:
obtain ⟨li, lj, hli, hlj, fac⟩ := h₃ _ hf

Goal state after:
J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
prop_id : D.W (𝟙 e)
h₁ : ∀ ⦃j : J⦄, D.P j → ∃ lift, D.W lift
h₂ : ∀ ⦃j : J⦄, D.P j → ∀ (l₁ l₂ : j ⟶ e), D.W l₁ → D.W l₂ → l₁ = l₂
h₃ : ∀ ⦃i j : J⦄ (f : i ⟶ j), D.W f → ∃ li lj, D.W li ∧ D.W lj ∧ f ≫ lj = li
i✝ j✝ : J
x✝ : i✝ ⟶ j✝
hf : D.W x✝
li : i✝ ⟶ e
lj : j✝ ⟶ e
hli : D.W li
hlj : D.W lj
fac : x✝ ≫ lj = li
⊢ x✝ ≫ ⋯.choose = ⋯.choose
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
inst✝⁶ : HasPushouts C
inst✝⁵ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝³ : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝² : OrderBot κ.ord.ToType
inst✝¹ : HasIterationOfShape κ.ord.ToType C
inst✝ : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
⊢ W.isLocal.ι.IsRightAdjoint

Tactic:
by
  rw [Functor.isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top]
  ext Z
  simpa using! (corepresentableBy Z hW).isCorepresentable

Goal state after:
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 π'
⊢ EffectiveEpi (π' ≫ π)

Tactic:
rw [effectiveEpi_iff_effectiveEpiFamily, ← Sieve.effectiveEpimorphic_family]
  suffices h₂ : (Sieve.generate (Presieve.ofArrows _ _)) ∈ (regularTopology C) X by
    change Nonempty _
    rw [← Sieve.forallYonedaIsSheaf_iff_colimit]
    exact fun W => regularTopology.isSheaf_yoneda_obj W _ h₂
  apply Coverage.Saturate.transitive X (Sieve.generate (Presieve.ofArrows (fun () ↦ Y)
      (fun () ↦ π)))
  · apply Coverage.Saturate.of
    use Y, π
  · intro V f ⟨Y₁, h, g, ⟨hY, hf⟩⟩
    rw [← hf, Sieve.pullback_comp]
    apply (regularTopology C).pullback_stable'
    apply regularTopology.mem_sieves_of_hasEffectiveEpi
    cases hY
    exact ⟨Y', π', inferInstance, Y', (𝟙 _), π' ≫ π, Presieve.ofArrows.mk (), (by simp)⟩

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

Goal state before:
pp: case refine_2.of.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (generate (Presieve.ofArrows (fun x ↦ ∐ fun i ↦ X i) fun x ↦ Sigma.desc f)).arrows f_1 →
      (extensiveCoverage C ⊔ regularCoverage C).Saturate Y_1 (Sieve.pullback f_1 (generate (Presieve.ofArrows X f)))

Tactic:
rintro R g ⟨W, ψ, σ, ⟨⟩, rfl⟩
        change _ ∈ ((extensiveCoverage C) ⊔ (regularCoverage C)).toGrothendieck R
        rw [Sieve.pullback_comp]
        apply pullback_stable
        have : generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i) ≤
            (generate (Presieve.ofArrows X f)).pullback (Sigma.desc f) := by
          rintro Q q ⟨E, e, r, ⟨hq, rfl⟩⟩
          exact ⟨E, e, r ≫ (Sigma.desc f), by cases hq; simpa using Presieve.ofArrows.mk _, by simp⟩
        apply Coverage.saturate_of_superset _ this
        apply Coverage.Saturate.of
        refine Or.inl ⟨I, inferInstance, _, _, ⟨rfl, ?_⟩⟩
        convert! IsIso.id _
        aesop

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

Goal state before:
pp: case mp.of.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S : Sieve X✝
X : C
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h' : IsIso (Sigma.desc π)
a : α
⊢ (Sieve.generate (Presieve.ofArrows Y π)).arrows (π a)

Tactic:
exact ⟨Y a, 𝟙 Y a, π a, Presieve.ofArrows.mk a, by simp⟩

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

Goal state before:
pp: 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)
⊢ IsIso (Sigma.desc π)

Tactic:
← show _ ↔ IsIso (Sigma.desc π) from
        Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc (c := Cofan.mk X π)

Goal state after:
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)
⊢ Nonempty (IsColimit (Cofan.mk 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 :
  ∀
    (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
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π
⊢ ∃! x, (ConcreteCategory.hom (P.map π.op)) x = b

Tactic:
have hb' : P.map (pullback.fst π π).op b = P.map (pullback.snd _ _).op b := by
    rw [← h₁, op_comp, Functor.map_comp, comp_apply, hb]
    simp [← comp_apply, ← Functor.map_comp, ← op_comp]

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
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π
hb' : (ConcreteCategory.hom (P.map (pullback.fst π π).op)) b = (ConcreteCategory.hom (P.map (pullback.snd π π).op)) b
⊢ ∃! x, (ConcreteCategory.hom (P.map π.op)) x = b
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP : EqualizerCondition P
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
h : Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯))
⊢ IsIso (equalizer.lift (P.map π.op) ⋯)

Tactic:
← isIso_iff_bijective,

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP : EqualizerCondition P
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
h : IsIso (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)
⊢ IsIso (equalizer.lift (P.map π.op) ⋯)
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))
⊢ Sheaf.IsLocallySurjective (c.π.app (op 0))

Tactic:
by
  rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff]
  intro X y
  have hh : EffectiveEpi (limit.π (preimageDiagram hF X y) ⟨0⟩) :=
    h _ fun n ↦ by simpa [preimageDiagram] using (preimageStruct hF X y).effectiveEpi n
  refine ⟨limit (preimageDiagram hF X y), limit.π (preimageDiagram hF X y) ⟨0⟩, hh,
    (coherentTopology C).yonedaEquiv (hc.lift (cone hF X y )),
    (?_ : (c.π.app (op 0)).hom.app _ _ = _)⟩
  simp only [← (coherentTopology C).yonedaEquiv_comp, cone,
    IsLimit.fac, NatTrans.ofOpSequence_app, (coherentTopology C).yonedaEquiv_comp,
    (coherentTopology C).yonedaEquiv_yoneda_map]
  rfl

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₃

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₃)
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
φ : Y ⟶ (sq₃ i₁ i₂ i₃).pullback
left✝¹ : φ ≫ (sq₃ i₁ i₂ i₃).p₁ = f₁
left✝ : φ ≫ (sq₃ i₁ i₂ i₃).p₂ = f₂
right✝ : φ ≫ (sq₃ i₁ i₂ i₃).p₃ = f₃
⊢ pullHom' hom q f₁ f₂ ⋯ ⋯ ≫ pullHom' hom q f₂ f₃ ⋯ ⋯ = pullHom' hom q f₁ f₃ ⋯ ⋯
Module: Mathlib.CategoryTheory.Sites.LocalProperties

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
i : ι
g : I₁.Y ⟶ X i
⊢ IsIso (f.hom.app (op r.Z))

Tactic:
exact hiso r.Z i (r.g₁ ≫ g)

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.map (p ≫ f₁).op.toLoc).toFunctor.map (hom w hf' φ i₁) =
    (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom q f₁ f₂ ⋯ ⋯) ≫
        (F.map p.op.toLoc).toFunctor.map ((F.map f₂.op.toLoc).toFunctor.map (hom w hf' φ i₂)) ≫
          (F.map p.op.toLoc).toFunctor.map (D₂.hom q f₂ f₁ ⋯ ⋯) ≫
            (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₁)

Tactic:
← F.mapComp'_naturality_1 f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc (by grind),

Goal state after:
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.map (p ≫ f₁).op.toLoc).toFunctor.map (hom w hf' φ i₁) =
    (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom q f₁ f₂ ⋯ ⋯) ≫
        ((F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂) ≫
            (F.map (p ≫ f₂).op.toLoc).toFunctor.map (hom w hf' φ i₂) ≫
              (F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₂)) ≫
          (F.map p.op.toLoc).toFunctor.map (D₂.hom q f₂ f₁ ⋯ ⋯) ≫
            (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₁)
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
this✝ : (pullFunctor F ⋯).Faithful
this : (pullFunctor F ⋯).Full
⊢ (pullFunctor F ⋯).FullyFaithful

Tactic:
exact .ofFullyFaithful _

Goal state after:
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ : OneCochain G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁ γ₂ α
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ (ConcreteCategory.hom (G.map a.op)) (α⁻¹ i) * ((ConcreteCategory.hom (G.map a.op)) (α i) * γ₁.ev i j a b) =
    γ₁.ev i j a b * ((ConcreteCategory.hom (G.map b.op)) (α⁻¹ j) * (ConcreteCategory.hom (G.map b.op)) (α j))

Tactic:
Cochain₀.inv_apply,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ : OneCochain G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁ γ₂ α
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ (ConcreteCategory.hom (G.map a.op)) (α i)⁻¹ * ((ConcreteCategory.hom (G.map a.op)) (α i) * γ₁.ev i j a b) =
    γ₁.ev i j a b * ((ConcreteCategory.hom (G.map b.op)) (α⁻¹ j) * (ConcreteCategory.hom (G.map b.op)) (α j))