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

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m₀ : ι → J
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
t₁ : (i : ι) → m₀ i ⟶ m₁ := fun i ↦ toMax m₀ hι i
u : (i : ι) → (D i).top ⟶ m₁ := fun i ↦ t₀ i ≫ t₁ i
S : Type (max 0 w) := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
shape : MultispanShape :=
  { L := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }, R := PUnit.{w + 1}, fst := fun x ↦ PUnit.unit,
    snd := fun x ↦ PUnit.unit }
index : MultispanIndex shape J :=
  { left := fun x ↦ (↑x).2.2, right := fun x ↦ m₁, fst := fun x ↦ (D (↑x).1).isTerminal.lift ⋯ ≫ u (↑x).1,
    snd := fun x ↦ (D (↑x).2.1).isTerminal.lift ⋯ ≫ u (↑x).2.1 }
hκ : Cardinal.aleph0 ≤ κ
hL : HasCardinalLT shape.L κ
hR : HasCardinalLT shape.R κ
⊢ ∃ m u,
    (∀ (i : ι), IsEmpty (m ⟶ (D i).top)) ∧
      ∀ (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₂

Tactic:
have hshape : HasCardinalLT (Arrow (WalkingMultispan shape)) κ := by
    rw [hasCardinalLT_iff_of_equiv (WalkingMultispan.arrowEquiv shape),
      hasCardinalLT_sum_iff _ _ _ hκ, hasCardinalLT_sum_iff _ _ _ hκ,
      hasCardinalLT_iff_of_equiv (WalkingMultispan.equiv shape),
      hasCardinalLT_sum_iff _ _ _ hκ]
    refine ⟨⟨?_, ?_⟩, ?_, ?_⟩ <;> assumption

Goal state after:
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
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
t₁ : (i : ι) → m₀ i ⟶ m₁ := fun i ↦ toMax m₀ hι i
u : (i : ι) → (D i).top ⟶ m₁ := fun i ↦ t₀ i ≫ t₁ i
S : Type (max 0 w) := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
shape : MultispanShape :=
  { L := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }, R := PUnit.{w + 1}, fst := fun x ↦ PUnit.unit,
    snd := fun x ↦ PUnit.unit }
index : MultispanIndex shape J :=
  { left := fun x ↦ (↑x).2.2, right := fun x ↦ m₁, fst := fun x ↦ (D (↑x).1).isTerminal.lift ⋯ ≫ u (↑x).1,
    snd := fun x ↦ (D (↑x).2.1).isTerminal.lift ⋯ ≫ u (↑x).2.1 }
hκ : Cardinal.aleph0 ≤ κ
hL : HasCardinalLT shape.L κ
hR : HasCardinalLT shape.R κ
hshape : HasCardinalLT (Arrow (WalkingMultispan shape)) κ
⊢ ∃ m u,
    (∀ (i : ι), IsEmpty (m ⟶ (D i).top)) ∧
      ∀ (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₂
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: case mp.top
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
⊢ ∃ Y_1 π, EffectiveEpi π ∧ ⊤.arrows π

Tactic:
exact ⟨Y, (𝟙 Y), inferInstance, by simp only [Sieve.top_apply]⟩

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
⊢ IsLocallySurjective φ ↔ Epi φ

Tactic:
by
  constructor
  · intro
    infer_instance
  · intro
    let data := (locallySurjective J A).factorizationData (locallyInjective J A) φ
    have : IsLocallySurjective data.i := data.hi
    have : IsLocallyInjective data.p := data.hp
    have : Epi data.p := epi_of_epi_fac data.fac
    have := mono_of_isLocallyInjective data.p
    have := isIso_of_mono_of_epi data.p
    rw [← data.fac]
    infer_instance

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

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (coherentTopology C) (Functor.whiskerRight f (forget D)) →
    Presheaf.IsLocallySurjective (regularTopology C) f

Tactic:
Presheaf.isLocallySurjective_iff_whisker_forget (J := regularTopology C)

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (coherentTopology C) (Functor.whiskerRight f (forget D)) →
    Presheaf.IsLocallySurjective (regularTopology C) (Functor.whiskerRight f (forget D))
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve B := (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows
X' : S.category := S.categoryMk π ⋯
P' : S.category := S.categoryMk (c.fst ≫ π) ⋯
fst : P' ⟶ X' := ObjectProperty.homMk (Over.homMk c.fst ⋯)
snd : P' ⟶ X' := ObjectProperty.homMk (Over.homMk c.snd ⋯)
F : S.categoryᵒᵖ ⥤ D := S.diagram.op ⋙ P
G : WalkingParallelPair ⥤ D := parallelPair (P.map c.fst.op) (P.map c.snd.op)
H : WalkingParallelPair ⥤ S.categoryᵒᵖ := parallelPair fst.op snd.op
this : H.Initial
⊢ (H ⋙ F).map WalkingParallelPairHom.left ≫ (Iso.refl ((H ⋙ F).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((H ⋙ F).obj WalkingParallelPair.zero)).hom ≫ G.map WalkingParallelPairHom.left

Tactic:
by aesop

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve B := (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows
X' : S.category := S.categoryMk π ⋯
P' : S.category := S.categoryMk (c.fst ≫ π) ⋯
fst : P' ⟶ X' := ObjectProperty.homMk (Over.homMk c.fst ⋯)
snd : P' ⟶ X' := ObjectProperty.homMk (Over.homMk c.snd ⋯)
F : S.categoryᵒᵖ ⥤ D := S.diagram.op ⋙ P
G : WalkingParallelPair ⥤ D := parallelPair (P.map c.fst.op) (P.map c.snd.op)
H : WalkingParallelPair ⥤ S.categoryᵒᵖ := parallelPair fst.op snd.op
this : H.Initial
⊢ (H ⋙ F).map WalkingParallelPairHom.right ≫ (Iso.refl ((H ⋙ F).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((H ⋙ F).obj WalkingParallelPair.zero)).hom ≫ G.map WalkingParallelPairHom.right

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ f₁.op.toLoc ≫ g.op.toLoc = gf₁.op.toLoc

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ f₂.op.toLoc ≫ g.op.toLoc = gf₂.op.toLoc

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
Y'' : C
g' : Y'' ⟶ Y'
g'f₁ : Y'' ⟶ X₁
g'f₂ : Y'' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
hg'f₁ : g' ≫ gf₁ = g'f₁
hg'f₂ : g' ≫ gf₂ = g'f₂
⊢ gf₂.op.toLoc ≫ g'.op.toLoc = g'f₂.op.toLoc

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
Y'' : C
g' : Y'' ⟶ Y'
g'f₁ : Y'' ⟶ X₁
g'f₂ : Y'' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
hg'f₁ : g' ≫ gf₁ = g'f₁
hg'f₂ : g' ≫ gf₂ = g'f₂
⊢ gf₁.op.toLoc ≫ g'.op.toLoc = g'f₁.op.toLoc

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
S : C
R : Sieve S
hR : R ∈ J S
⊢ F.IsStackFor R.arrows

Tactic:
(Tactic.tacticSeq
 (Tactic.tacticSeq1Indented
  [(Tactic.rwSeq "rw" (Tactic.optConfig []) (Tactic.rwRuleSeq "[" [(Tactic.rwRule [] `isStackFor_iff)] "]") [])
   []
   (Tactic.tacticHave__
    "have"
    (Term.letConfig [])
    (Term.letDecl
     (Term.letIdDecl
      (Term.letId `hF)
      []
      []
      ":="
      (Term.proj
       (Term.paren
        (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
        (Term.app `F.isPrestackFor' [(Term.hole "_") `hR])
        ")")
       "."
       `fullyFaithful))))
   []
   (Tactic.tacticHave__
    "have"
    (Term.letConfig [])
    (Term.letDecl (Term.letIdDecl (Term.letId (hygieneInfo `[anonymous])) [] [] ":=" `hF.full)))
   []
   (Tactic.tacticHave__
    "have"
    (Term.letConfig [])
    (Term.letDecl (Term.letIdDecl (Term.letId (hygieneInfo `[anonymous])) [] [] ":=" `hF.faithful)))
   []
   (Tactic.tacticHave__
    "have"
    (Term.letConfig [])
    (Term.letDecl
     (Term.letIdDecl
      (Term.letId (hygieneInfo `[anonymous]))
      []
      []
      ":="
      (Term.app `IsStack.essSurj_of_sieve [`F (Term.hole "_") `hR]))))
   []
   (Tactic.exact
    "exact"
    (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))]))

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
S : C
R : Sieve S
hR : R ∈ J S
⊢ F.IsStackFor R.arrows

Tactic:
(Term.byTactic
 "by"
 (Tactic.tacticSeq
  (Tactic.tacticSeq1Indented
   [(Tactic.rwSeq "rw" (Tactic.optConfig []) (Tactic.rwRuleSeq "[" [(Tactic.rwRule [] `isStackFor_iff)] "]") [])
    []
    (Tactic.tacticHave__
     "have"
     (Term.letConfig [])
     (Term.letDecl
      (Term.letIdDecl
       (Term.letId `hF)
       []
       []
       ":="
       (Term.proj
        (Term.paren
         (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
         (Term.app `F.isPrestackFor' [(Term.hole "_") `hR])
         ")")
        "."
        `fullyFaithful))))
    []
    (Tactic.tacticHave__
     "have"
     (Term.letConfig [])
     (Term.letDecl (Term.letIdDecl (Term.letId (hygieneInfo `[anonymous])) [] [] ":=" `hF.full)))
    []
    (Tactic.tacticHave__
     "have"
     (Term.letConfig [])
     (Term.letDecl (Term.letIdDecl (Term.letId (hygieneInfo `[anonymous])) [] [] ":=" `hF.faithful)))
    []
    (Tactic.tacticHave__
     "have"
     (Term.letConfig [])
     (Term.letDecl
      (Term.letIdDecl
       (Term.letId (hygieneInfo `[anonymous]))
       []
       []
       ":="
       (Term.app `IsStack.essSurj_of_sieve [`F (Term.hole "_") `hR]))))
    []
    (Tactic.exact
     "exact"
     (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))])))

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
i : ι
Z : C
q : Z ⟶ X i
hq : (sieve f f' i).arrows (Over.homMk q ⋯)
⊢ ∃ j a, a ≫ f' j = q ≫ f i

Tactic:
by
  obtain ⟨_, q, _, ⟨j⟩, fac⟩ := hq
  exact ⟨j, q, fac⟩

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₂
i : ι
Z : Over (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
j : ι'
a : Z.left ⟶ X' j
fac : autoParam (a ≫ f' j = Z.hom ≫ f i) familyOfElements_eq._auto_1
⊢ g = Over.homMk Z.hom ⋯

Tactic:
ext; simpa using Over.w g

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
s : ↑(presheafHom F G).sections
X : C
Y : Over X
H : (ConcreteCategory.hom ((presheafHom F G).map Y.hom.op)) (↑s (op X)) = ↑s (op Y.left)
⊢ (↑s (op Y.left)).app (op (Over.mk (𝟙 Y.left))) = (↑s (op X)).app (op Y)

Tactic:
← H

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
s : ↑(presheafHom F G).sections
X : C
Y : Over X
H : (ConcreteCategory.hom ((presheafHom F G).map Y.hom.op)) (↑s (op X)) = ↑s (op Y.left)
⊢ ((ConcreteCategory.hom ((presheafHom F G).map Y.hom.op)) (↑s (op X))).app (op (Over.mk (𝟙 Y.left))) =
    (↑s (op X)).app (op Y)
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₂
i : ι'
⊢ D₁.hom (f' i) (p' i) (p' i) ⋯ ⋯ ≫ pullHom (φ.hom i) (𝟙 (X' i)) (p' i) (p' i) ⋯ ⋯ ≫ D₂.hom (f' i) (p' i) (p' i) ⋯ ⋯ =
    φ.hom i

Tactic:
pullHom_id,

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₂
i : ι'
⊢ D₁.hom (f' i) (p' i) (p' i) ⋯ ⋯ ≫ φ.hom i ≫ D₂.hom (f' i) (p' i) (p' i) ⋯ ⋯ = φ.hom i
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
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
⊢ (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)

Tactic:
simpa [← Category.assoc] using (sheafificationAdjunction J D).counit_naturality f

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✝
M M' M'' : C ⥤ MonCat
S : SubmonoidFunctor M
S' : SubmonoidFunctor M'
x✝³ : Set (SubmonoidFunctor M)
x✝² : SubmonoidFunctor M
x✝¹ : x✝² ∈ upperBounds x✝³
x✝ : C
⊢ { obj := fun x ↦ ⨆ F ∈ x✝³, F.obj x, map := ⋯ }.obj x✝ ≤ x✝².obj x✝

Tactic:
by aesop

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✝
M M' M'' : C ⥤ MonCat
S : SubmonoidFunctor M
S' : SubmonoidFunctor M'
x✝⁴ : Set (SubmonoidFunctor M)
x✝³ : SubmonoidFunctor M
x✝² : x✝³ ∈ x✝⁴
x✝¹ : C
x✝ : ↑(M.obj x✝¹)
⊢ x✝ ∈ { obj := fun x ↦ ⨅ F ∈ x✝⁴, F.obj x, map := ⋯ }.obj x✝¹ → x✝ ∈ x✝³.obj x✝¹

Tactic:
by aesop

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✝
M M' M'' : C ⥤ MonCat
S : SubmonoidFunctor M
S' : SubmonoidFunctor M'
x✝³ : Set (SubmonoidFunctor M)
x✝² : SubmonoidFunctor M
x✝¹ : x✝² ∈ lowerBounds x✝³
x✝ : C
⊢ x✝².obj x✝ ≤ { obj := fun x ↦ ⨅ F ∈ x✝³, F.obj x, map := ⋯ }.obj x✝

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M : C ⥤ MonCat
⊢ image (𝟙 M) ⊤ = ⊤

Tactic:
by aesop

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
⊢ image S.ι (comap S.ι S) = S

Tactic:
by aesop

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
S : C
R : Sieve S
M N : ↑(F.obj { as := op S })
X : C
g : X ⟶ S
f : Over.mk g ⟶ Over.mk (𝟙 S)
hf : R.arrows (Over.Hom.left f)
⊢ f = Over.homMk g ⋯

Tactic:
ext; simpa using Over.w f

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U X : C
m : U ⟶ X
x✝ : Mono m
χ₀ : U ⟶ ⊤_ C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (h.isoΩ₀.inv ≫ h.Ω₀.arrow)
⊢ χ' = h.χ m

Tactic:
have : IsPullback m (h.χ₀ U) χ' h.Ω₀.arrow :=
      sq.of_iso (Iso.refl _) (Iso.refl _) (h.isoΩ₀.symm) (Iso.refl _)
        (by simp) (h.isTerminalΩ₀.hom_ext _ _) (by simp) (by simp)
    exact h.uniq this

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

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
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (F.map
        ((shiftFunctorCompIsoId C n (-n) ⋯).inv.app (unop X) ≫
          ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop)).op =
    (commShiftIso F.op n).hom.app (op ((shiftFunctor C n).obj (unop X))) ≫
      (shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).inv.app (unop X)).op ≫
        (shiftFunctorOpIso D n (-n) ⋯).hom.app (op ((shiftFunctor D n).obj (F.obj (unop X)))) ≫
          ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op

Tactic:
F.op_commShiftIso_hom_app_assoc _ _ _ (add_neg_cancel n),

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (F.map
        ((shiftFunctorCompIsoId C n (-n) ⋯).inv.app (unop X) ≫
          ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop)).op =
    (F.map ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop).op ≫
      ((commShiftIso F (-n)).inv.app (unop (op ((shiftFunctor C n).obj (unop X))))).op ≫
        (shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop (op ((shiftFunctor C n).obj (unop X)))))) ≫
          (shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).inv.app (unop X)).op ≫
            (shiftFunctorOpIso D n (-n) ⋯).hom.app (op ((shiftFunctor D n).obj (F.obj (unop X)))) ≫
              ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
x₂ : X₂ ⟶ B
hx₂ : f₁ ≫ x₂ = 0
⊢ (Triangle.mk (ι.map f₁) f₂ f₃).mor₁ ≫ ι.map x₂ = 0

Tactic:
by simp [← ι.map_comp, hx₂]

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : ThreeGPFree s
ha : a ≠ 0
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : (fun x ↦ a • x) b * (fun x ↦ a • x) d = (fun x ↦ a • x) c * (fun x ↦ a • x) c
⊢ b * d = c * c

Tactic:
by simpa [mul_mul_mul_comm _ _ a, ha] using h

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

Goal state before:
pp: case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
⊢ ThreeAPFree (sphere x 0)

Tactic:
rw [sphere_zero]

Goal state after:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
⊢ ThreeAPFree {x}
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ (a + b) i < 2 * d - 1

Tactic:
lt_tsub_iff_right,

Goal state after:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ (a + b) i + 1 < 2 * d
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
h : s.prod = t.prod
hf : IsMulFreimanHom (0 + 1) A B f
hs : s.card = 0
x✝ : t.card = 0
⊢ (map f s).prod = (map f t).prod

Tactic:
by aesop

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

Goal state before:
pp: x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ x + 1 ≤ rexp (1 - x) / rexp (-2 * x)

Tactic:
← exp_sub,

Goal state after:
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ x + 1 ≤ rexp (1 - x - -2 * x)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ x + 1 ≤ rexp (1 - x - -(2 * x))

Tactic:
sub_neg_eq_add,

Goal state after:
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ x + 1 ≤ rexp (1 - x + 2 * x)