mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X✝ Y✝ X Y : F C
h : X ⟶ Y
η' : F C
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ h ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
this :
  (normalizeIsoApp' C η' (X.normalizeObj n)).hom =
    eqToHom ⋯ ≫ (normalizeIsoApp' C η' (Y.normalizeObj n)).hom ≫ eqToHom ⋯
⊢ (α_ (inclusionObj n) X η').inv ≫
      ((normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)) ▷ η' ≫ (normalizeIsoApp' C η' (Y.normalizeObj n)).hom =
    ((α_ (inclusionObj n) X η').inv ≫
        (normalizeIsoApp' C X n).hom ▷ η' ≫ (normalizeIsoApp' C η' (X.normalizeObj n)).hom) ≫
      inclusion.map (eqToHom ⋯)

Tactic:
simp [this]

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

Goal state before:
pp: case e'_3
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x : ↑A
⊢ x = 1 • x

Tactic:
one_smul

Goal state after:
case e'_3
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x : ↑A
⊢ x = x
Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
i : ι
hf : Arrow.mk (f i) ∈ (ofHoms f).toSet
⊢ ∃ a, (fun i ↦ ⟨Arrow.mk (f i), ⋯⟩) a = ⟨Arrow.mk (f i), hf⟩

Tactic:
exact ⟨i, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : P.isLocal g
hfg : P.localEpi (f ≫ g)
T : C
hT : P T
v : Y ⟶ T
u : Z ⟶ T
huv : (fun g ↦ f ≫ g) ((fun g_1 ↦ g ≫ g_1) u) = (fun g ↦ f ≫ g) v
⊢ (fun g_1 ↦ g ≫ g_1) u = v

Tactic:
obtain ⟨v, rfl⟩ := (hg _ hT).surjective v

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : P.isLocal g
hfg : P.localEpi (f ≫ g)
T : C
hT : P T
u v : Z ⟶ T
huv : (fun g ↦ f ≫ g) ((fun g_1 ↦ g ≫ g_1) u) = (fun g ↦ f ≫ g) ((fun g_1 ↦ g ≫ g_1) v)
⊢ (fun g_1 ↦ g ≫ g_1) u = (fun g_1 ↦ g ≫ g_1) v
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ →o (Subobject X)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
G : ℕ ⥤ (MonoOver X)ᵒᵖ
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      { toFun := (G ⋙ (Subobject.equivMonoOver X).inverse.op ⋙ (orderDualEquivalence (Subobject X)).inverse).obj,
            monotone' := ⋯ }
          n =
        { toFun := (G ⋙ (Subobject.equivMonoOver X).inverse.op ⋙ (orderDualEquivalence (Subobject X)).inverse).obj,
            monotone' := ⋯ }
          m
m : ℕ
hm : n ⟶ m
⊢ Subobject.mk (Opposite.unop (G.obj m)).obj.hom = Subobject.mk (Opposite.unop (G.obj n)).obj.hom

Tactic:
exact (hn m (leOfHom hm)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ IsNoetherianObject X ↔ ∀ (F : ℕ ⥤ MonoOver X), IsFiltered.IsEventuallyConstant F

Tactic:
rw [isNoetherianObject_iff_monotone_chain_condition]
  refine ⟨fun h G ↦ ?_, fun h F ↦ ?_⟩
  · obtain ⟨n, hn⟩ := h (G ⋙ (Subobject.equivMonoOver _).inverse).toOrderHom
    refine ⟨n, fun m hm ↦ ?_⟩
    rw [MonoOver.isIso_iff_subobjectMk_eq]
    exact hn m (leOfHom hm)
  · obtain ⟨n, hn⟩ := h (F.monotone.functor ⋙ Subobject.representative)
    refine ⟨n, fun m hm ↦ ?_⟩
    simpa [← MonoOver.isIso_iff_isIso_hom_left, isIso_iff_of_reflects_iso,
      PartialOrder.isIso_iff_eq] using hn (homOfLE hm)

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D
F₁ : C₁ ⥤ D
F₂ : C₂ ⥤ D
P₁ : ObjectProperty C₁
P₂ : ObjectProperty C₂
inst✝² : ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂
inst✝ : LocallySmall.{w, v_3, u_3} D
Q₁ : ObjectProperty C₁
w✝¹ : ObjectProperty.Small.{w, v_1, u_1} Q₁
h₁ : Q₁ ≤ P₁
h₁' : P₁ ≤ Q₁.isoClosure
Q₂ : ObjectProperty C₂
w✝ : ObjectProperty.Small.{w, v_2, u_2} Q₂
h₂ : Q₂ ≤ P₂
h₂' : P₂ ≤ Q₂.isoClosure
f : Comma F₁ F₂
hf : P₁ f.left ∧ P₂ f.right
X₁ : C₁
hX₁ : Q₁ X₁
e₁ : f.left ≅ X₁
X₂ : C₂
hX₂ : Q₂ X₂
e₂ : f.right ≅ X₂
⊢ comma F₁ F₂ Q₁ Q₂ { left := X₁, right := X₂, hom := F₁.map e₁.inv ≫ f.hom ≫ F₂.map e₂.hom }

Tactic:
tauto

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : ι → C
κ : Cardinal.{w}
h : HasCardinalLT ι κ
i : ι
⊢ ∃ a, (fun i ↦ ⟨X i, ⋯⟩) a = ⟨X i, ⋯⟩

Tactic:
exact ⟨i, rfl⟩

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

Goal state before:
pp: case pos
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 α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ⟨b, ⋯⟩ = ⟨a, j_property✝⟩
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 𝟙 (s (f b))

Tactic:
cases h

Goal state after:
case pos.refl
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 α
f : α → ι
b : α
j_property✝ : b ∈ f ⁻¹' {f b}
j_property : f b = f b
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a ↦ s (f a)) b ≫ biproduct.π (fun b ↦ s (f b)) b = 𝟙 (s (f b))
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ ↑x✝¹.succ • x✝ = ↑x✝¹ • x✝ + x✝

Tactic:
simp_rw [HSMul.hSMul, SMul.smul]; ext <;> dsimp <;> simp [add_zsmul]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
f : End X
hf : f ≠ 0
this : IsIso f
⊢ inv f ≫ f = 𝟙 X

Tactic:
exact IsIso.inv_hom_id f

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

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = if Nonempty (X ≅ Y) then 1 else 0

Tactic:
split_ifs with h
  · exact (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y).2 h
  · exact (finrank_hom_simple_simple_eq_zero_iff 𝕜 X Y).2 (not_nonempty_iff.mp h)

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

Goal state before:
pp: case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : (f j).ι
⊢ eqToHom ⋯ = eqToHom ⋯ x (⋯ ▸ x)

Tactic:
simp only [CategoryTheory.eqToHom_refl, CategoryTheory.Mat_.id_apply_self]

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

Goal state before:
pp: 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

Tactic:
tauto

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

Goal state before:
pp: case neg.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').ι
h : ¬i' = i
⊢ ¬(i = i' ∧ j ≍ j')

Tactic:
tauto

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : F.Additive
L : Mat_ C ⥤ D
inst✝ : L.Additive
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ (additiveObjIsoBiproduct L X✝).hom ≫
      (biproduct.matrix fun j k ↦
          L.map ((embedding C).map (f j k)) ≫ (α.app (Y✝.X k)).hom ≫ ((embeddingLiftIso F).symm.app (Y✝.X k)).hom) ≫
        (additiveObjIsoBiproduct (lift F) Y✝).inv =
    (additiveObjIsoBiproduct L X✝).hom ≫
      (biproduct.map fun b ↦ (α.app (X✝.X b)).hom) ≫
        (biproduct.map fun b ↦ ((embeddingLiftIso F).symm.app (X✝.X b)).hom) ≫
          (biproduct.matrix fun i j ↦ (lift F).map ((embedding C).map (f i j))) ≫
            (additiveObjIsoBiproduct (lift F) Y✝).inv

Tactic:
simp only [biproduct.map_matrix_assoc]

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : F.Additive
L : Mat_ C ⥤ D
inst✝ : L.Additive
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ (additiveObjIsoBiproduct L X✝).hom ≫
      (biproduct.matrix fun j k ↦
          L.map ((embedding C).map (f j k)) ≫ (α.app (Y✝.X k)).hom ≫ ((embeddingLiftIso F).symm.app (Y✝.X k)).hom) ≫
        (additiveObjIsoBiproduct (lift F) Y✝).inv =
    (additiveObjIsoBiproduct L X✝).hom ≫
      (biproduct.matrix fun j k ↦
          (α.app (X✝.X j)).hom ≫
            ((embeddingLiftIso F).symm.app (X✝.X j)).hom ≫ (lift F).map ((embedding C).map (f j k))) ≫
        (additiveObjIsoBiproduct (lift F) Y✝).inv
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case refine_1
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j x✝ : J
h : __Diagram✝.P x✝
⊢ ∃ lift, __Diagram✝.W lift

Tactic:
simp only [Diagram.single_P, ObjectProperty.singleton_iff] at h
      subst h
      exact ⟨𝟙 _, ⟨⟨⟩⟩⟩

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

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
⊢ ∀ (j_1 : J) (hj : (Diagram.single j).IsTerminal j_1), j_1 = j

Tactic:
rintro _ ⟨⟨⟩⟩; rfl

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

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
⊢ Monotone Subtype.val

Tactic:
tauto

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

Goal state before:
pp: X✝ X : Type u
⊢ IsPresentable.{u, u, u + 1} X

Tactic:
by
  obtain ⟨κ, hκ, hX⟩ := HasCardinalLT.exists_regular_cardinal.{u} X
  have : Fact κ.IsRegular := ⟨hκ⟩
  have := hX.isCardinalPresentable
  exact isPresentable_of_isCardinalPresentable X κ

Goal state after:
Module: Mathlib.CategoryTheory.RegularCategory.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f : X ⟶ Y
m : coequalizer (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
⊢ pullback.fst f f ≫ e = d ≫ k₁

Tactic:
by simp [d, k₁]

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
R : F.RepresentableBy X
⊢ F.IsRepresentedBy (R.homEquiv (𝟙 X))

Tactic:
rw [IsRepresentedBy.iff_isIso_uliftYonedaEquiv]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
R : F.RepresentableBy X
⊢ IsIso (uliftYonedaEquiv.symm { down := R.homEquiv (𝟙 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
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : Presieve.ofArrows Y π x✝
⊢ S.arrows x✝

Tactic:
cases h

Goal state after:
case mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
i✝ : α
⊢ S.arrows (π i✝)
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
this : IsCardinalFiltered J Cardinal.aleph0
⊢ ∃ α x, ∃ (_ : IsDirected α fun x1 x2 ↦ x1 ≤ x2) (_ : Nonempty α), ∃ F, F.Final

Tactic:
obtain ⟨α, _, _, F, _⟩ := IsCardinalFiltered.exists_cardinal_directed J .aleph0

Goal state after:
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
this : IsCardinalFiltered J Cardinal.aleph0
α : Type w
w✝¹ : PartialOrder α
w✝ : IsCardinalFiltered α Cardinal.aleph0
F : α ⥤ J
h✝ : F.Final
⊢ ∃ α x, ∃ (_ : IsDirected α fun x1 x2 ↦ x1 ≤ x2) (_ : Nonempty α), ∃ F, F.Final
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

Goal state after:
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 := ⋯
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) := ⋯
⊢ (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a) ∈ (extensiveCoverage C).coverings (⊥_ C)
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.SheafComparison

Goal state before:
pp: 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
⊢ F.IsCoverDense (regularTopology D)

Tactic:
by
  refine F.isCoverDense_of_generate_singleton_functor_π_mem _ fun B ↦ ⟨_, F.effectiveEpiOver B, ?_⟩
  apply Coverage.Saturate.of
  refine ⟨F.effectiveEpiOverObj B, F.effectiveEpiOver B, ?_, inferInstance⟩
  funext; ext -- Do we want `Presieve.ext`?
  refine ⟨fun ⟨⟩ ↦ ⟨()⟩, ?_⟩
  rintro ⟨⟩
  simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra f
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    D₁.hom i₁ i₂ ≫ (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom) =
      (e i₁).hom ≫ D₂.hom i₁ i₂
i₁ i₂ : ι
⊢ D₂.hom i₁ i₂ ≫ (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).inv) =
    (e i₁).inv ≫ D₁.hom i₁ i₂

Tactic:
rw [← cancel_epi (e i₁).hom, ← reassoc_of% (comm i₁ i₂), ← Functor.map_comp, ← Functor.map_comp]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra f
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    D₁.hom i₁ i₂ ≫ (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom) =
      (e i₁).hom ≫ D₂.hom i₁ i₂
i₁ i₂ : ι
⊢ D₁.hom i₁ i₂ ≫
      (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map ((e i₂).hom ≫ (e i₂).inv)) =
    (e i₁).hom ≫ (e i₁).inv ≫ D₁.hom i₁ i₂
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
⊢ IsPullback fst snd f g

Tactic:
suffices IsIso (pullback.lift fst snd h) from
    .of_iso_pullback ⟨h⟩ (asIso (pullback.lift _ _ h)) (by simp) (by simp)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
⊢ IsIso (pullback.lift fst snd h)
Module: Mathlib.CategoryTheory.Sites.Point.IsMonoidalW

Goal state before:
pp: C : Type u
inst✝¹⁴ : Category.{v, u} C
inst✝¹³ : LocallySmall.{w, v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝¹² : Category.{v', u'} A
inst✝¹¹ : MonoidalCategory A
inst✝¹⁰ : HasColimitsOfSize.{w, w, v', u'} A
inst✝⁹ : HasProducts A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁸ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁷ : ConcreteCategory A FC
inst✝⁶ : HasWeakSheafify J A
inst✝⁵ : (forget A).ReflectsIsomorphisms
inst✝⁴ : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
inst✝³ : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst✝² : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : J.HasEnoughPoints
⊢ J.W.IsMonoidal

Tactic:
by
  obtain ⟨P, _, hP⟩ := HasEnoughPoints.exists_objectProperty J
  exact hP.isMonoidal_W A

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
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
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ (F.map f₁.op.toLoc).toFunctor.map
        ((F.mapComp' (p' (β k₁)).op.toLoc (q' k₁).op.toLoc (r' k₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α (β k₁)))) ≫
      (F.mapComp' (r' k₁).op.toLoc f₁.op.toLoc ((r' k₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app
          (D.obj (α (β k₁))) ≫
        D.hom (s ≫ r) (f₁ ≫ r' k₁) (f₂ ≫ r' k₂) ⋯ ⋯ ≫
          (F.mapComp' (r' k₂).op.toLoc f₂.op.toLoc ((r' k₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
            (D.obj (α (β k₂))) =
    (F.mapComp' (q' k₁).op.toLoc f₁.op.toLoc ((q' k₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app
        ((F.map (p' (β k₁)).op.toLoc).toFunctor.obj (D.obj (α (β k₁)))) ≫
      (F.mapComp' (p' (β k₁)).op.toLoc ((q' k₁).op.toLoc ≫ f₁.op.toLoc) ((r' k₁).op.toLoc ≫ f₁.op.toLoc)
                  ⋯).inv.toNatTrans.app
          (D.obj (α (β k₁))) ≫
        D.hom (s ≫ r) (f₁ ≫ r' k₁) (f₂ ≫ r' k₂) ⋯ ⋯ ≫
          (F.mapComp' (p' (β k₂)).op.toLoc ((q' k₂).op.toLoc ≫ f₂.op.toLoc) ((r' k₂).op.toLoc ≫ f₂.op.toLoc)
                      ⋯).hom.toNatTrans.app
              (D.obj (α (β k₂))) ≫
            (F.mapComp' (q' k₂).op.toLoc f₂.op.toLoc ((q' k₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
                ((F.map (p' (β k₂)).op.toLoc).toFunctor.obj (D.obj (α (β k₂)))) ≫
              (F.map f₂.op.toLoc).toFunctor.map
                ((F.mapComp' (p' (β k₂)).op.toLoc (q' k₂).op.toLoc (r' k₂).op.toLoc ⋯).inv.toNatTrans.app
                  (D.obj (α (β k₂))))

Tactic:
rw [mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc _ _ _ _ _ _ _
        (by grind) rfl rfl, mapComp'₀₂₃_hom_app _ _ _ _ _ _ _ _ rfl rfl]

Goal state after: