mathlib-initiative/mathlib-tactics huggingface dataset:
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
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ J S
⊢ Nonempty (F.toDescentData f).FullyFaithful

Tactic:
rw [← isPrestackFor_ofArrows_iff, ← IsPrestackFor_generate_iff,
      isPrestackFor_iff_isSheafFor]

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
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ J S
⊢ ∀ (M N : ↑(F.obj { as := op S })),
    Presieve.IsSheafFor (F.presheafHom M N)
      ((Sieve.overEquiv (Over.mk (𝟙 S))).symm (Sieve.generate (Presieve.ofArrows X f))).arrows
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ 𝒞.χ i ≫ (Iso.refl 𝒞.Ω).hom = (Iso.refl X).hom ≫ 𝒞.χ i

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ 𝒞.truth ≫ (Iso.refl 𝒞.Ω).hom = (Iso.refl 𝒞.Ω₀).hom ≫ 𝒞.truth

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ pullback.snd 𝒞.truth (𝒞.χ i) ≫ 𝟙 X =
    (underlyingIso (pullback.snd 𝒞.truth (𝒞.χ i))).inv ≫ ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow

Tactic:
Iso.eq_inv_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ (underlyingIso (pullback.snd 𝒞.truth (𝒞.χ i))).hom ≫ pullback.snd 𝒞.truth (𝒞.χ i) ≫ 𝟙 X =
    ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
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
𝒞 : Classifier C
X✝ : C
φ : X✝ ⟶ 𝒞.Ω
⊢ (fun x ↦ 𝒞.χ (arrow x)) ((fun φ ↦ (pullback φ).obj 𝒞.truth_as_subobject) φ) = φ

Tactic:
by simp

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
𝒞 : Classifier C
X✝ : C
x : (Subobject.presheaf C).obj (Opposite.op X✝)
⊢ (fun φ ↦ (pullback φ).obj 𝒞.truth_as_subobject) ((fun x ↦ 𝒞.χ (arrow x)) x) = x

Tactic:
by simp

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 Ω
X : C
π' : X ⟶ underlying.obj h.Ω₀
⊢ ∀ (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow), s.fst ≫ 𝟙 X = s.fst

Tactic:
by simp

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
⊢ m ≫ (Iso.refl X✝).hom = (Iso.refl U✝).hom ≫ m

Tactic:
by simp

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
⊢ h.χ m ≫ (Iso.refl Ω).hom = (Iso.refl X✝).hom ≫ h.χ m

Tactic:
by simp

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
⊢ h.Ω₀.arrow ≫ (Iso.refl Ω).hom = h.isoΩ₀.hom ≫ h.isoΩ₀.inv ≫ h.Ω₀.arrow

Tactic:
by simp

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)
⊢ m ≫ (Iso.refl X).hom = (Iso.refl U).hom ≫ m

Tactic:
by simp

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)
⊢ χ' ≫ (Iso.refl Ω).hom = (Iso.refl X).hom ≫ χ'

Tactic:
by simp

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.isoΩ₀.inv ≫ h.Ω₀.arrow) ≫ (Iso.refl Ω).hom = h.isoΩ₀.symm.hom ≫ h.Ω₀.arrow

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ IsPullback (m.hom ≫ 𝟙 G.obj) ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom (Presheaf.χ m.hom)
    (Subfunctor.lift (Presheaf.truth C) ⋯ ≫ (closedSieves J).ι)

Tactic:
simp only [Category.comp_id]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ IsPullback m.hom ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom (Presheaf.χ m.hom)
    (Subfunctor.lift (Presheaf.truth C) ⋯ ≫ (closedSieves J).ι)
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

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✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
⊢ (F.mapTriangle.obj (Triangle.mk (G.map T.mor₁) f g)).mor₁ ≫ adj.counit.app T.obj₂ = adj.counit.app T.obj₁ ≫ T.mor₁

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
⊢ CommSq (𝟙 G.obj) χ'.hom (χ'.hom ≫ (closedSieves J).ι) (closedSieves J).ι

Tactic:
by simp

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 ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
T : Triangle C
⊢ ((triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T))).mor₁ ≫
      (Iso.refl ((triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T))).obj₂).hom =
    (Iso.refl ((triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T))).obj₁).hom ≫
      (F.op.mapTriangle.obj ((triangleOpEquivalence C).functor.obj (op T))).mor₁

Tactic:
by simp

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 ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
T : Triangle C
⊢ ((triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T))).mor₂ ≫
      (Iso.refl ((triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T))).obj₃).hom =
    (Iso.refl ((triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T))).obj₂).hom ≫
      (F.op.mapTriangle.obj ((triangleOpEquivalence C).functor.obj (op T))).mor₂

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ ((opOp C).mapTriangle.obj T).mor₁ ≫ (Iso.refl ((opOp C).mapTriangle.obj T).obj₂).hom =
    (Iso.refl ((opOp C).mapTriangle.obj T).obj₁).hom ≫
      ((triangleOpEquivalence Cᵒᵖ).functor.obj (op ((triangleOpEquivalence C).functor.obj (op T)))).mor₁

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ ((opOp C).mapTriangle.obj T).mor₂ ≫ (Iso.refl ((opOp C).mapTriangle.obj T).obj₃).hom =
    (Iso.refl ((opOp C).mapTriangle.obj T).obj₂).hom ≫
      ((triangleOpEquivalence Cᵒᵖ).functor.obj (op ((triangleOpEquivalence C).functor.obj (op T)))).mor₂

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

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✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
φ : Y ⟶ G.obj T.obj₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁ = ψ ≫ g
α : Y ⟶ G.obj T.obj₃
hα : α = φ - ψ ≫ (adj.homEquiv Z T.obj₃) h
hα₀ : α ≫ G.map T.mor₃ = 0
β : Y ⟶ Z
hβ : β ≫ (adj.homEquiv Z T.obj₃) h = α
⊢ (ψ + β) ≫ (adj.homEquiv Z T.obj₃) h = φ

Tactic:
add_comp,

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✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
φ : Y ⟶ G.obj T.obj₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁ = ψ ≫ g
α : Y ⟶ G.obj T.obj₃
hα : α = φ - ψ ≫ (adj.homEquiv Z T.obj₃) h
hα₀ : α ≫ G.map T.mor₃ = 0
β : Y ⟶ Z
hβ : β ≫ (adj.homEquiv Z T.obj₃) h = α
⊢ ψ ≫ (adj.homEquiv Z T.obj₃) h + β ≫ (adj.homEquiv Z T.obj₃) h = φ
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
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
hT' : Triangle.mk (𝟙 ((shiftFunctor C 1).obj (ι.obj X₁))) 0 0 ∈ distinguishedTriangles
⊢ IsLimit (KernelFork.ofι f₁ ⋯)

Tactic:
refine IsLimit.ofIsoLimit (AbelianSubcategory.isLimitKernelFork hι
    (rot_of_distTriang _ hT) hT') ?_

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
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
hT' : Triangle.mk (𝟙 ((shiftFunctor C 1).obj (ι.obj X₁))) 0 0 ∈ distinguishedTriangles
⊢ KernelFork.ofι
      (ιK (-(shiftFunctor C 1).map (Triangle.mk (ι.map f₁) (ι.map f₂) f₃).mor₁) (𝟙 ((shiftFunctor C 1).obj (ι.obj X₁))))
      ⋯ ≅
    KernelFork.ofι f₁ ⋯
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
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
hT' : Triangle.mk (𝟙 ((shiftFunctor C 1).obj (ι.obj X₁))) 0 0 ∈ distinguishedTriangles
⊢ (ι ⋙ shiftFunctor C 1).map
      ((-Iso.refl
              (KernelFork.ofι
                  (ιK (-(shiftFunctor C 1).map (Triangle.mk (ι.map f₁) (ι.map f₂) f₃).mor₁)
                    (𝟙 ((shiftFunctor C 1).obj (ι.obj X₁))))
                  ⋯).pt).hom ≫
        Fork.ι (KernelFork.ofι f₁ ⋯)) =
    (ι ⋙ shiftFunctor C 1).map
      (Fork.ι
        (KernelFork.ofι
          (ιK (-(shiftFunctor C 1).map (Triangle.mk (ι.map f₁) (ι.map f₂) f₃).mor₁)
            (𝟙 ((shiftFunctor C 1).obj (ι.obj X₁))))
          ⋯))

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: case refine_2
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
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
⊢ IsZero (contractibleTriangle (ι.obj X₃)).invRotate.obj₁

Tactic:
dsimp
      rw [IsZero.iff_id_eq_zero, ← Functor.map_id, id_zero, Functor.map_zero]

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
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
hT' : Triangle.mk 0 (𝟙 (ι.obj X₃)) 0 ∈ distinguishedTriangles
⊢ ι.map
      (Cofork.π (CokernelCofork.ofπ (πQ (ι.map f₂) (𝟙 (ι.obj X₃))) ⋯) ≫
        (Iso.refl (CokernelCofork.ofπ (πQ (ι.map f₂) (𝟙 (ι.obj X₃))) ⋯).pt).hom) =
    ι.map (Cofork.π (CokernelCofork.ofπ f₂ ⋯))

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
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:
simpa [mul_mul_mul_comm _ _ a] using h

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
r : α → β → Prop
h₁ : LeftTotal r
h₂ : LeftUnique r
⊢ ∀ a ∈ univ, ∃ b ∈ univ, r a b

Tactic:
by simpa using! h₁

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
r : α → β → Prop
h₁ : RightTotal r
h₂ : RightUnique r
⊢ ∀ b ∈ univ, ∃ a ∈ univ, r a b

Tactic:
by simpa using! h₁

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

Goal state before:
pp: α : Type u_2
inst✝ : CommMonoid α
A : Set α
n : ℕ
s t : Multiset α
x✝³ : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
x✝² : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
x✝¹ : s.card = n
x✝ : t.card = n
⊢ (map id s).prod = (map id t).prod ↔ s.prod = t.prod

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
k : Fin (n + 1)
⊢ ↑(range ↑k) ⊆ Set.Iio n.succ

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
k : Fin (n + 1)
x : Fin n.succ
hx : ↑x < ↑k
⊢ ↑↑x = x

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
A : Set X
⊢ ↑(#1) ≤ 1 ∧ A ⊆ ↑1 • A

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
N : Type u_2
X : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : MulAction M X
inst✝² : MulAction N X
K L : ℝ
A B C : Set X
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : ↑(#F₁) ≤ K
hFAB : A ⊆ ↑F₁ • B
F₂ : Finset N
hF₂ : ↑(#F₂) ≤ L
hFBC : B ⊆ ↑F₂ • C
⊢ ↑F₁ • ↑F₂ • C = ↑(F₁ • F₂) • C

Tactic:
by simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
A : Set α
B : Set β
n✝ : ℕ
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hfAB : MapsTo (⇑f) A B
n : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n + 1
ht : t.card = n + 1
h : s.prod = t.prod
⊢ (map (⇑f) s).prod = (map (⇑f) t).prod

Tactic:
by
    rw [← map_multiset_ne_zero_prod _ (by grind [Multiset.card_eq_zero]),
        h, map_multiset_ne_zero_prod _ (by grind [Multiset.card_eq_zero])]

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 - -2 * x)

Tactic:
neg_mul,

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.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}
F : Finset G
hFmax : Maximal (fun x ↦ x ⊆ A ∧ (↑x).PairwiseDisjoint fun x ↦ x • B) F
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
b : G
hb : b ∈ F
c : G
hc₁ : a⁻¹ • c ∈ B
hc₂ : b⁻¹ • c ∈ B
⊢ b⁻¹ • c / a⁻¹ • c = b⁻¹ * a

Tactic:
by simp

Goal state after:
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}
F : Finset G
hFmax : Maximal (fun x ↦ x ⊆ A ∧ (↑x).PairwiseDisjoint fun x ↦ x • B) F
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
b : G
hb : b ∈ F
c : G
hc₁ : a⁻¹ • c ∈ B
hc₂ : b⁻¹ • c ∈ B
⊢ b * (b⁻¹ * a) = a

Tactic:
by simp

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

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ 0 < 8

Tactic:
by simp

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

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ 1 < 8

Tactic:
by simp

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

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 2 ≤ 8

Tactic:
by simp

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

Goal state before:
pp: N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (↑(nValue N))⁻¹
⊢ (2 * ↑(dValue N)) ^ nValue N ≤ ↑N

Tactic:
rw [← rpow_natCast]

Goal state after:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (↑(nValue N))⁻¹
⊢ (2 * ↑(dValue N)) ^ ↑(nValue N) ≤ ↑N