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

Goal state before:
pp: case refine_2.inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
⊢ ∃ lift,
    (((⨆ i, (D i).W) ⊔ MorphismProperty.ofHoms fun x ↦ 𝟙 m) ⊔
        MorphismProperty.ofHoms fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst)
      lift

Tactic:
exact ⟨𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩)⟩

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₁
⊢ ∃ lift, (D₄ D φ).W lift

Tactic:
exact ⟨𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩)⟩

Goal state after:
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)
⊢ 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

Tactic:
apply Coverage.Saturate.transitive X (Sieve.generate (Presieve.ofArrows Y π))

Goal state after:
case a
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)
⊢ (coherentCoverage C).Saturate X (Sieve.generate (Presieve.ofArrows Y π))

case a
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)
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
    (Sieve.generate (Presieve.ofArrows Y π)).arrows f →
      (coherentCoverage C).Saturate Y_1
        (Sieve.pullback f
          (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)))
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
⊢ IsSheaf (extensiveTopology C) F → PreservesFiniteProducts F

Tactic:
intro h
    rw [IsSheaf] at h
    refine ⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩
    constructor
    apply coyonedaJointlyReflectsLimits
    intro ⟨E⟩
    specialize h E
    rw [Presieve.isSheaf_iff_preservesFiniteProducts] at h
    exact isLimitOfPreserves (F.comp (coyoneda.obj ⟨E⟩)) hc

Goal state after:
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
i : J
⊢ PreservesFiniteProducts ((G ⋙ sheafToPresheaf (extensiveTopology C) A).obj i)

Tactic:
rw [← Presheaf.isSheaf_iff_preservesFiniteProducts]
    exact (G.obj i).property

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

Goal state before:
pp: case refine_2
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.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (coherentTopology D) (F.obj X)
α : Type
w✝ : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
let Z : α → C := fun a ↦ (Functor.EffectivelyEnough.presentation (F := F) (Y a)).some.p

Goal state after:
case refine_2
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.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (coherentTopology D) (F.obj X)
α : Type
w✝ : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun a ↦ ⋯.some.p
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_2.refine_2
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.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (coherentTopology D) (F.obj X)
α : Type
w✝ : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun a ↦ ⋯.some.p
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun a ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily (fun a ↦ F.obj (Z a)) fun a ↦ g₀ a ≫ π a
a : α
⊢ S.arrows (F.preimage (g₀ a ≫ π a))

Tactic:
obtain ⟨W, g₁, g₂, h₁, h₂⟩ := H₂ a
      rw [h₂]
      convert! S.downward_closed h₁ (F.preimage (g₀ a ≫ g₂))
      exact F.map_injective (by simp)

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP : ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)
⊢ EqualizerCondition P

Tactic:
apply EqualizerCondition.mk

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP : ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)
⊢ ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯))
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
X✝ Y✝ : ↑(F.obj { as := op S }).obj
g : X✝ ⟶ Y✝
i₁ i₂ : ι
⊢ { obj := fun i ↦ (F.map (f i).op.toLoc).l.toFunctor.obj X✝,
            hom := fun i₁ i₂ ↦
              (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app X✝),
            counit := ⋯, coassoc := ⋯ }.hom
        i₁ i₂ ≫
      (F.map (f i₁).op.toLoc).l.toFunctor.map
        ((F.map (f i₂).op.toLoc).r.toFunctor.map ((F.map (f i₂).op.toLoc).l.toFunctor.map g)) =
    (F.map (f i₁).op.toLoc).l.toFunctor.map g ≫
      { obj := fun i ↦ (F.map (f i).op.toLoc).l.toFunctor.obj Y✝,
            hom := fun i₁ i₂ ↦
              (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app Y✝),
            counit := ⋯, coassoc := ⋯ }.hom
        i₁ i₂

Tactic:
by simp [← Functor.map_comp]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
⊢ Multifork.IsLimit.lift hE (fun a ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫
      (E.multifork G).ι (g.s₀ i) ≫ G.map (g.h₀ i).op =
    t.ι i

Tactic:
Multifork.IsLimit.fac_assoc,

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
⊢ (t.ι (f.s₀ (g.s₀ i)) ≫ G.map (f.h₀ (g.s₀ i)).op) ≫ G.map (g.h₀ i).op = t.ι i
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
D : F.DescentData f
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S'
q' : Y' ⟶ S'
hq : g ≫ q = q'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
gf₁ : Y' ⟶ X' j₁
gf₂ : Y' ⟶ X' j₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ (f₁ ≫ p' j₁) ≫ f (α j₁) = q ≫ p

Tactic:
by rw [Category.assoc, w, reassoc_of% hf₁]

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
D : F.DescentData f
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S'
q' : Y' ⟶ S'
hq : g ≫ q = q'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
gf₁ : Y' ⟶ X' j₁
gf₂ : Y' ⟶ X' j₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ (F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app
        ((F.map (p' j₁).op.toLoc).toFunctor.obj (D.obj (α j₁))) ≫
      (F.map g.op.toLoc).toFunctor.map
          ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc ((p' j₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app
            (D.obj (α j₁))) ≫
        (F.map g.op.toLoc).toFunctor.map (D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯) ≫
          (F.map g.op.toLoc).toFunctor.map
              ((F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc ((p' j₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
                (D.obj (α j₂))) ≫
            (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).inv.toNatTrans.app
              ((F.map (p' j₂).op.toLoc).toFunctor.obj (D.obj (α j₂))) =
    (F.mapComp' (p' j₁).op.toLoc gf₁.op.toLoc ((p' j₁).op.toLoc ≫ gf₁.op.toLoc) ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      (F.mapComp' ((p' j₁).op.toLoc ≫ f₁.op.toLoc) g.op.toLoc ((p' j₁).op.toLoc ≫ gf₁.op.toLoc) ⋯).hom.toNatTrans.app
          (D.obj (α j₁)) ≫
        (F.map g.op.toLoc).toFunctor.map (D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯) ≫
          (F.mapComp' ((p' j₂).op.toLoc ≫ f₂.op.toLoc) g.op.toLoc ((p' j₂).op.toLoc ≫ gf₂.op.toLoc)
                      ⋯).inv.toNatTrans.app
              (D.obj (α j₂)) ≫
            (F.mapComp' (p' j₂).op.toLoc gf₂.op.toLoc ((p' j₂).op.toLoc ≫ gf₂.op.toLoc) ⋯).hom.toNatTrans.app
              (D.obj (α j₂))

Tactic:
rw [F.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app_assoc _ _ _ _ _ _ _ _ (by cat_disch),
      mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app _ _ _ _ _ _ _ _ _ (by cat_disch)]

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
D₁ D₂ : F.DescentData f
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ (f₁ ≫ p' j₁) ≫ f (α j₁) = q ≫ p

Tactic:
by rw [Category.assoc, w, reassoc_of% hf₁]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
X : C
R : Presieve X
h : R ∈ K.coverings X
h' : Presieve.IsSheafFor F R
G : Subfunctor F := K.subsheafify 𝒮
⊢ Presieve.IsSheafFor (K.subsheafify 𝒮).toFunctor R

Tactic:
rw [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
X : C
R : Presieve X
h : R ∈ K.coverings X
h' : Presieve.IsSheafFor F R
G : Subfunctor F := K.subsheafify 𝒮
⊢ Presieve.IsSeparatedFor (K.subsheafify 𝒮).toFunctor R ∧
    ∀ (x : Presieve.FamilyOfElements (K.subsheafify 𝒮).toFunctor R), x.Compatible → ∃ t, x.IsAmalgamation t
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 : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor F S.arrows

Tactic:
rw [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]

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 : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSeparatedFor F S.arrows ∧
    ∀ (x : Presieve.FamilyOfElements F S.arrows), x.Compatible → ∃ t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
x : F.obj (Opposite.op X)
Z✝ : C
a✝ : F.obj (Opposite.op Z✝)
ha : a✝ ∈ 𝒮 Z✝
⊢ Witness.eval hF ι t (Witness.base Z✝ ((equivShrink ↑(𝒮 Z✝)) ⟨a✝, ha⟩)) = some a✝

Tactic:
by grind [Witness.eval]

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M : C ⥤ MonCat
S : SubmonoidFunctor M
U V : C
f : U ⟶ V
⊢ S.obj U ≤ Submonoid.comap (MonCat.Hom.hom (M.map f)) (S.obj V)

Tactic:
S.map f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
M : C ⥤ MonCat
S : SubmonoidFunctor M
U V : C
f : U ⟶ V
⊢ Submonoid.comap (MonCat.Hom.hom (M.map f)) (S.obj V) ≤ Submonoid.comap (MonCat.Hom.hom (M.map f)) (S.obj V)
Module: Mathlib.CategoryTheory.Sites.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
⊢ IsRegularEpi f

Tactic:
obtain ⟨I, p, i, hp, hi, hpi⟩ := h f
    -- The sheafification of `f.hom` is `f` pre- and postcomposed with isomorphisms.
    have h₁ : (presheafToSheaf J D).map f.hom =
          (sheafificationAdjunction J D).counit.app F ≫ f ≫
          inv ((sheafificationAdjunction J D).counit.app G) := by
        simpa [← Category.assoc] using (sheafificationAdjunction J D).counit_naturality f
    have h₂ : f = inv ((sheafificationAdjunction J D).counit.app F) ≫
        (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G := by
      simp [h₁]
    -- The sheafification of `f.val` is still an epimorphism
    have : Epi ((presheafToSheaf J D).map f.hom) := by
      rw [h₁]
      infer_instance
    -- The sheafification of `i` is an epimorphism, because the sheafification of `p ≫ i = f.val`
    -- is an epimorphism.
    have : Epi ((presheafToSheaf J D).map i) := by
      rw [← hpi, Functor.map_comp] at this
      exact epi_of_epi ((presheafToSheaf J D).map p) _
    -- Since the sheafification of `i` is both a monomorphism and an epimorphism, it is an
    -- isomorphism.
    have : IsIso ((presheafToSheaf J D).map i) :=
      Balanced.isIso_of_mono_of_epi _
    -- The next five lines show that it suffices to show that the sheafification of `p` is a
    -- regular epimorphism.
    rw [h₂, isRegularEpi_iff_effectiveEpi]
    suffices EffectiveEpi ((presheafToSheaf J D).map f.hom) by infer_instance
    rw [← hpi, Functor.map_comp]
    suffices EffectiveEpi ((presheafToSheaf J D).map p) by infer_instance
    rw [← isRegularEpi_iff_effectiveEpi]
    -- The underlying presheaf of the kernel pair of `f` is a kernel pair for `p`, and since
    -- sheafification preserves colimits, `p` exhibits its target `I` as a coequalizer of this
    -- kernel pair. The result follows.
    exact ⟨⟨{
      W := (presheafToSheaf J D).obj (pullback f f).obj
      left := (presheafToSheaf J D).map (pullback.fst f f).hom
      right := (presheafToSheaf J D).map (pullback.snd f f).hom
      w := by
        rw [← Functor.map_comp, ← Functor.map_comp]
        congr 1
        rw [← cancel_mono i]
        simp [hpi, ← ObjectProperty.FullSubcategory.comp_hom, pullback.condition]
      isColimit := by
        have := IsRegularEpiCategory.regularEpiOfEpi p
        exact isColimitCoforkMapOfIsColimit (presheafToSheaf J D) _
          (isColimitCoforkOfEffectiveEpi p _
            (PullbackCone.isLimitOfFactors f.hom f.hom i _ _ hpi hpi _
              ((isLimitPullbackConeMapOfIsLimit (sheafToPresheaf _ _) _
                (pullbackIsPullback f f))))) }⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
X : C
x : Subobject X
⊢ (Subobject.pullback (h.homEquiv.symm x)).obj h.Ω₀ = x

Tactic:
rw [← homEquiv_eq, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ (S.sequence F n₀ n₁ h).map' 1 2 _proof_246✝ _proof_451✝ ≫ (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝)).hom =
    ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom ≫
      (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 1 2 _proof_246✝ _proof_451✝

Tactic:
by ext; symm; apply mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ (S.sequence F n₀ n₁ h).map' 4 5 _proof_453✝ _proof_454✝ ≫ (Iso.refl ((S.sequence F n₀ n₁ h).obj' 5 _proof_454✝)).hom =
    ((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom ≫
      (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 4 5 _proof_453✝ _proof_454✝

Tactic:
by ext; symm; apply mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
this : ThreeGPFree ↑(image f s)
⊢ #(image f s) ≤ mulRothNumber B

Tactic:
refine this.le_mulRothNumber ?_

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
this : ThreeGPFree ↑(image f s)
⊢ image f s ⊆ B
Module: Mathlib.Combinatorics.Additive.ETransform

Goal state before:
pp: case snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 ∩ e⁻¹ • x.1 ∩ (x.2 ∪ e⁻¹ • x.1) = x.2 ∩ e⁻¹ • x.1

Tactic:
inter_eq_left

Goal state after:
case snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 ∩ e⁻¹ • x.1 ⊆ x.2 ∪ e⁻¹ • x.1
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
⊢ minOrder G = ⊤

Tactic:
simpa [minOrder] using fun _ ↦ not_isOfFinOrder_of_isMulTorsionFree

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁✝ : ↑u
hs : v₁✝ ∈ u ↓∩ s
v₂✝ : ↑u
ht : v₂✝ ∈ u ↓∩ t
⊢ (SimpleGraph.induce u G).Adj v₁✝ v₂✝

Tactic:
comap_adj,

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁✝ : ↑u
hs : v₁✝ ∈ u ↓∩ s
v₂✝ : ↑u
ht : v₂✝ ∈ u ↓∩ t
⊢ G.Adj ((Embedding.subtype fun x ↦ x ∈ u) v₁✝) ((Embedding.subtype fun x ↦ x ∈ u) v₂✝)
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case neg
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
w : α
hw : w ∈ s
hwx : f w < f x
⊢ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
refine ⟨f w, fun y hy => ⟨Nat.le_of_succ_le_succ ?_, hs hy hw⟩⟩

Goal state after:
case neg
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : s.EquitableOn f
w : α
hw : w ∈ s
hwx : f w < f x
y : α
hy : y ∈ s
⊢ (f w).succ ≤ (f y).succ
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
⊢ Fintype.card α / #P.parts - Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts ≤ 4 ^ #P.parts - 1

Tactic:
tsub_le_iff_left,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
⊢ Fintype.card α / #P.parts ≤ Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts + (4 ^ #P.parts - 1)