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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X)
j j' : (Over (unop (op X)))ᵒᵖ
φ : j ⟶ j'
⊢ uncurry
      ((f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op)) ≫
        (pre (F.map (Over.Hom.left φ.unop).op)).app (G.obj (op (unop j').left))) =
    uncurry
      ((f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)) ≫
        (ihom (F.obj (op (unop j).left))).map (G.map (Over.Hom.left φ.unop).op))

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X)
j j' : (Over (unop (op X)))ᵒᵖ
φ : j ⟶ j'
⊢ uncurry
      (f ≫
        enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op) ≫
          (pre (F.map (Over.Hom.left φ.unop).op)).app (G.obj (op (unop j').left))) =
    uncurry
      ((f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)) ≫
        (ihom (F.obj (op (unop j).left))).map (G.map (Over.Hom.left φ.unop).op))
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X)
j j' : (Over (unop (op X)))ᵒᵖ
φ : j ⟶ j'
⊢ uncurry
      (f ≫
        enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op) ≫
          (pre (F.map (Over.Hom.left φ.unop).op)).app (G.obj (op (unop j').left))) =
    uncurry
      ((f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)) ≫
        (ihom (F.obj (op (unop j).left))).map (G.map (Over.Hom.left φ.unop).op))

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X)
j j' : (Over (unop (op X)))ᵒᵖ
φ : j ⟶ j'
⊢ uncurry
      (f ≫
        enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op) ≫
          (pre (F.map (Over.Hom.left φ.unop).op)).app (G.obj (op (unop j').left))) =
    uncurry
      (f ≫
        enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op) ≫
          (ihom (F.obj (op (unop j).left))).map (G.map (Over.Hom.left φ.unop).op))
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
hG : IsSheaf J G
X : C
S : Sieve X
⊢ S ∈ J X → Presieve.IsSheafFor (presheafHom F G) S.arrows

Tactic:
hS

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
hG : IsSheaf J G
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor (presheafHom F G) S.arrows
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
N : Type u'
inst✝² : Category.{v', u'} N
p : N ⥤ C
inst✝¹ : InitiallySmall N
J : GrothendieckTopology C
inst✝ : IsCofiltered N
⊢ ∀ {d : (fiber p).Elements} {c : N} (s s' : (functor p).obj c ⟶ d),
    ∃ c' t, (functor p).map t ≫ s = (functor p).map t ≫ s'

Tactic:
rintro ⟨X, x⟩ V ⟨φ₁, hφ₁⟩ ⟨φ₂, hφ₂⟩

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
N : Type u'
inst✝² : Category.{v', u'} N
p : N ⥤ C
inst✝¹ : InitiallySmall N
J : GrothendieckTopology C
inst✝ : IsCofiltered N
X : C
x : (fiber p).obj X
V : N
φ₁ : ((functor p).obj V).fst ⟶ ⟨X, x⟩.fst
hφ₁ : (hom ((fiber p).map φ₁)) ((functor p).obj V).snd = ⟨X, x⟩.snd
φ₂ : ((functor p).obj V).fst ⟶ ⟨X, x⟩.fst
hφ₂ : (hom ((fiber p).map φ₂)) ((functor p).obj V).snd = ⟨X, x⟩.snd
⊢ ∃ c' t, (functor p).map t ≫ ⟨φ₁, hφ₁⟩ = (functor p).map t ≫ ⟨φ₂, hφ₂⟩
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 : autoParam (q ≫ p = r) pullFunctorCompIso._auto_1
hr' : autoParam (∀ (k : ι''), q' k ≫ p' (β k) = r' k) pullFunctorCompIso._auto_3
k : ι''
⊢ (q' k ≫ p' (β k)) ≫ f (α (β k)) = f'' k ≫ r

Tactic:
Category.assoc,

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
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 : autoParam (q ≫ p = r) pullFunctorCompIso._auto_1
hr' : autoParam (∀ (k : ι''), q' k ≫ p' (β k) = r' k) pullFunctorCompIso._auto_3
k : ι''
⊢ q' k ≫ p' (β k) ≫ f (α (β k)) = f'' k ≫ r
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
inst✝ : ∀ (Z : C), _root_.Small.{max u v, w} (F.obj (Opposite.op Z))
X : C
S : Sieve X
⊢ S ∈ J X → Presieve.IsSheafFor F S.arrows

Tactic:
hS

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
inst✝ : ∀ (Z : C), _root_.Small.{max u v, w} (F.obj (Opposite.op Z))
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor F S.arrows
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
⊢ S ∈ J X → Presieve.IsSheafFor F S.arrows

Tactic:
hS

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.IsSheafFor F S.arrows
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)
⊢ Small.{max u v, w} ((K.subsheafify 𝒮).toFunctor.obj (Opposite.op X))

Tactic:
let t (X : C) (i : ι X) : F.obj (Opposite.op X) := ((equivShrink _).symm i).val

Goal state after:
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)
⊢ Small.{max u v, w} ((K.subsheafify 𝒮).toFunctor.obj (Opposite.op X))
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)
⊢ Small.{max u v, w} ((K.subsheafify 𝒮).toFunctor.obj (Opposite.op X))

Tactic:
have (x : F.obj (.op X)) (hx : K.SubsheafClosure 𝒮 X x) :
      ∃ (i : Witness K ι X), Witness.eval hF _ t i = x := by
    induction hx with
    | base ha => exact ⟨.base _ (equivShrink _ ⟨_, ha⟩), by grind [Witness.eval]⟩
    | restrict f ha ih =>
      obtain ⟨i, hi⟩ := ih
      use .restrict f i
      grind [Witness.eval]
    | amalgamate hR hy hmem ht ih =>
      choose x hx using ih
      exact ⟨.amalgamate hR x, by simp [Witness.eval, hx]; grind⟩

Goal state after:
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)
this : ∀ (x : F.obj (Opposite.op X)), K.SubsheafClosure 𝒮 X x → ∃ i, Witness.eval hF ι t i = some x
⊢ Small.{max u v, w} ((K.subsheafify 𝒮).toFunctor.obj (Opposite.op X))
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
K : Coverage C
h : K.Generates J
⊢ K.toGrothendieck = J

Tactic:
← Coverage.toGrothendieck_toPrecoverage

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
K : Coverage C
h : K.Generates J
⊢ K.toGrothendieck = J
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'
p : M ⟶ M'
S'' : SubmonoidFunctor M''
S' : SubmonoidFunctor M'
U✝ V✝ : C
x✝¹ : U✝ ⟶ V✝
x✝ : ↑(M.obj U✝)
h : x✝ ∈ Submonoid.comap (MonCat.Hom.hom (p.app U✝)) (S'.obj U✝)
⊢ x✝ ∈ Submonoid.comap (MonCat.Hom.hom (M.map x✝¹)) (Submonoid.comap (MonCat.Hom.hom (p.app V✝)) (S'.obj V✝))

Tactic:
by
    simp_rw [Submonoid.mem_comap, NatTrans.naturality_apply]
    exact Submonoid.mem_comap.mp (Set.mem_of_mem_of_subset h (S'.map _))

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 R' : Presieve S
h : Sieve.generate R = Sieve.generate R'
⊢ Nonempty (F.toDescentData fun f ↦ f.obj.hom).FullyFaithful ↔
    Nonempty (F.toDescentData fun f ↦ f.obj.hom).FullyFaithful

Tactic:
obtain ⟨_, _, f, rfl⟩ := Presieve.exists_eq_ofArrows R

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R' : Presieve S
w✝¹ : Type (max u v)
w✝ : w✝¹ → C
f : (i : w✝¹) → w✝ i ⟶ S
h : Sieve.generate (Presieve.ofArrows w✝ f) = Sieve.generate R'
⊢ Nonempty (F.toDescentData fun f_1 ↦ f_1.obj.hom).FullyFaithful ↔
    Nonempty (F.toDescentData fun f ↦ f.obj.hom).FullyFaithful
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 R' : Presieve S
h : Sieve.generate R = Sieve.generate R'
⊢ (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence ↔ (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence

Tactic:
obtain ⟨_, _, f, rfl⟩ := Presieve.exists_eq_ofArrows R

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R' : Presieve S
w✝¹ : Type (max u v)
w✝ : w✝¹ → C
f : (i : w✝¹) → w✝ i ⟶ S
h : Sieve.generate (Presieve.ofArrows w✝ f) = Sieve.generate R'
⊢ (F.toDescentData fun f_1 ↦ f_1.obj.hom).IsEquivalence ↔ (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
J : GrothendieckTopology C
hF : ∀ (S : C), ∀ R ∈ J S, F.IsPrestackFor R.arrows
S✝ : C
M N : ↑(F.obj { as := op S✝ })
U : Over S✝
S : Sieve U
⊢ S ∈ (J.over S✝) U → Presieve.IsSheafFor (F.presheafHom M N) S.arrows

Tactic:
hS

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
J : GrothendieckTopology C
hF : ∀ (S : C), ∀ R ∈ J S, F.IsPrestackFor R.arrows
S✝ : C
M N : ↑(F.obj { as := op S✝ })
U : Over S✝
S : Sieve U
hS : S ∈ (J.over S✝) U
⊢ Presieve.IsSheafFor (F.presheafHom M N) S.arrows
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✝³ : Preadditive C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
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 Y : A
n : ℤ
f : (shiftFunctor C n).obj (ι.obj X) ⟶ ι.obj Y
hn : 0 < n
⊢ (shiftFunctor C (-n)).map f = (shiftFunctor C (-n)).map 0

Tactic:
rw [← cancel_epi ((shiftEquiv C n).unitIso.hom.app _), Functor.map_zero, comp_zero]
    exact hι _ (by lia)

Goal state after:
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
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = (Triangle.mk (ι.map f₁) f₂ f₃).mor₃ ≫ l
⊢ k = 0

Tactic:
rw [eq_zero_of_hom_shift_pos hι l (by lia), comp_zero] at hl

Goal state after:
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
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = 0
⊢ k = 0
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
⊢ ∃ k, πQ f₂ β ≫ k = x₂

Tactic:
obtain ⟨x₁, hx₁⟩ := Triangle.yoneda_exact₂ _ hT (ι.map x₂) (by simp [← ι.map_comp, hx₂])
  obtain ⟨k, hk⟩ := Triangle.yoneda_exact₂ _ hT' x₁
    (eq_zero_of_hom_shift_pos hι _ (by lia))
  exact ⟨ι.preimage k, ι.map_injective (by cat_disch)⟩

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

Goal state before:
pp: case e'_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = mulRothNumber s
hu : ThreeGPFree ↑u
h : ThreeGPFree ↑(map (mulLeftEmbedding a) u)
⊢ mulRothNumber s = #(map (mulLeftEmbedding a) u)

Tactic:
rw [card_map, hcard]

Goal state after:
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
s t : Multiset (Fin (n + 1))
hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → x ∈ Iic ↑k
htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → x ∈ Iic ↑k
hs : s.card = m
ht : t.card = m
this : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1))) (map val u).sum = u.sum
⊢ (map val s).sum = (map val t).sum ↔
    (Nat.castRingHom (Fin (n + 1))) (map val s).sum = (Nat.castRingHom (Fin (n + 1))) (map val t).sum

Tactic:
have {u : Multiset (Fin (n + 1))} (huk : ∀ x ∈ u, x ≤ k) (hu : card u = m) :
        (u.map val).sum < (n + 1) := Nat.lt_succ_iff.2 <| hkmn.trans' <| by
      rw [← hu, ← card_map]
      refine sum_le_card_nsmul (u.map val) k ?_
      simpa [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, aux hm hkmn] using huk

Goal state after:
k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
s t : Multiset (Fin (n + 1))
hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → x ∈ Iic ↑k
htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → x ∈ Iic ↑k
hs : s.card = m
ht : t.card = m
this✝ : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1))) (map val u).sum = u.sum
this : ∀ {u : Multiset (Fin (n + 1))}, (∀ x ∈ u, x ≤ ↑k) → u.card = m → (map val u).sum < n + 1
⊢ (map val s).sum = (map val t).sum ↔
    (Nat.castRingHom (Fin (n + 1))) (map val s).sum = (Nat.castRingHom (Fin (n + 1))) (map val t).sum
Module: Mathlib.Combinatorics.Additive.RuzsaCovering

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F).PairwiseDisjoint fun x ↦ x • B}
⊢ (↑∅).PairwiseDisjoint fun x ↦ x • B

Tactic:
simp [coe_empty]

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

Goal state before:
pp: case hx
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N

Tactic:
cast_pos

Goal state after:
case hx
N : ℕ
hN : 4096 ≤ N
⊢ 0 < N
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #B * #(A⁻¹ * C) ≤ #(B⁻¹ * A) * #(B⁻¹ * C)

Tactic:
simpa [mul_comm, div_eq_mul_inv, ← map_op_mul, ← map_op_inv] using
    ruzsa_triangle_inequality_div_div_div (G := Gᵐᵒᵖ) (C.map opEquiv.toEmbedding)
      (B.map opEquiv.toEmbedding) (A.map opEquiv.toEmbedding)

Goal state after:
Module: Mathlib.Combinatorics.Additive.ETransform

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • x.2 * e⁻¹ • x.1 ⊆ x.1 * x.2

Tactic:
mul_smul_comm,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e⁻¹ • (e • x.2 * x.1) ⊆ x.1 * x.2
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∑ v ∈ G.support.toFinset, G.degree v = ∑ v ∈ G.support.toFinset, G.degree v + ∑ v ∈ G.support.toFinsetᶜ, G.degree v

Tactic:
left_eq_add

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∑ v ∈ G.support.toFinsetᶜ, G.degree v = 0
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
⊢ Odd #{w | w ≠ v ∧ Odd (G.degree w)}

Tactic:
rcases G.even_card_odd_degree_vertices with ⟨k, hg⟩

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
⊢ Odd #{w | w ≠ v ∧ Odd (G.degree w)}
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : H ↪g G
x✝¹ x✝ : W
⊢ (SimpleGraph.comap (⇑f) G).Adj x✝¹ x✝ ↔ H.Adj x✝¹ x✝

Tactic:
exact f.map_adj_iff

Goal state after:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Set α
f : α → ℕ
⊢ s.EquitableOn f ↔ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
refine ⟨?_, fun ⟨b, hb⟩ x y hx hy => by grw [(hb x hx).2, (hb y hy).1]⟩
  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
  · simp
  intro hs
  by_cases! h : ∀ y ∈ s, f x ≤ f y
  · exact ⟨f x, fun y hy => ⟨h _ hy, hs hy hx⟩⟩
  obtain ⟨w, hw, hwx⟩ := h
  refine ⟨f w, fun y hy => ⟨Nat.le_of_succ_le_succ ?_, hs hy hw⟩⟩
  rw [(Nat.succ_le_of_lt hwx).antisymm (hs hx hw)]
  exact hs hx hy

Goal state after:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case neg
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∀ x ∈ s, b + 1 = b + 1

Tactic:
exact fun _ _ => rfl

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this✝¹ : Lattice (Subtype Pr) := ⋯
this✝ : OrderBot (Subtype Pr) := ⋯
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage Subtype.val ⋯
i : Subtype Pr
hi : i ∈ P.parts.preimage Subtype.val ⋯
hi' : i ∉ t
this : (fun i ↦ ↑(id i)) = id ∘ Subtype.val
⊢ ↑(id i) ∈ P.parts

Tactic:
simpa using hi

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a✝ b c : α
ι : Type u_2
I : Finset ι
a : ι → α
P : (i : ι) → Finpartition (a i)
ha : I.SupIndep a
⊢ I.SupIndep fun i ↦ (P i).parts.sup id

Tactic:
by simpa only [sup_parts]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ¬b = c
d : α
hdb : d ∈ ((fun i ↦ Q ↑i ⋯) ⟨b, hb⟩).parts
hdc : d ∈ ((fun i ↦ Q ↑i ⋯) ⟨c, hc⟩).parts
⊢ False

Tactic:
exact
    (Q b hb).ne_bot hdb
      (eq_bot_iff.2 <|
        (le_inf ((Q b hb).le hdb) <| (Q c hc).le hdc).trans <| (P.disjoint hb hc hbc).le_bot)

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
hab : a < b
⊢ (P.extendOfLE ⋯).parts = insert (b \ a) P.parts

Tactic:
simp [extendOfLE, sdiff_eq_bot_iff.not.mpr (not_le_of_gt hab)]

Goal state after: