mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x y : (f j).ι
h' : ¬⋯ ▸ x = y
⊢ 0 = 𝟙 (f j) x y

Tactic:
id_apply_of_ne _ _ _ h'

Goal state after:
case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x y : (f j).ι
h' : ¬⋯ ▸ x = y
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h✝ : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
j : A
f g : J ⟶ F.obj j
h : f ≫ c.ι.app j = g ≫ c.ι.app j
k : ↑J.obj → A
a : (x : ↑J.obj) → j ⟶ k x
hk :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (F.map (a x))) (f.hom.hom' x) = (ConcreteCategory.hom (F.map (a x))) (g.hom.hom' x)
⊢ ∃ l c b, ∀ (x : ↑J.obj), a x ≫ b x = c

Tactic:
let φ (x : J.obj) : j ⟶ IsCardinalFiltered.max k hJ :=
          a x ≫ IsCardinalFiltered.toMax k hJ x

Goal state after:
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h✝ : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
j : A
f g : J ⟶ F.obj j
h : f ≫ c.ι.app j = g ≫ c.ι.app j
k : ↑J.obj → A
a : (x : ↑J.obj) → j ⟶ k x
hk :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (F.map (a x))) (f.hom.hom' x) = (ConcreteCategory.hom (F.map (a x))) (g.hom.hom' x)
φ : ↑J.obj → (j ⟶ IsCardinalFiltered.max k hJ) := fun x ↦ a x ≫ IsCardinalFiltered.toMax k hJ x
⊢ ∃ l c b, ∀ (x : ↑J.obj), a x ≫ b x = c
Module: Mathlib.CategoryTheory.Presentable.EssentiallyLarge

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : HasCardinalFilteredGenerator C κ
⊢ ∃ J x, Nonempty (C ≌ J)

Tactic:
by
  rw [exists_equivalence_iff_of_locallySmall]
  obtain ⟨P, _, hP⟩ := HasCardinalFilteredGenerator.exists_generator C κ
  exact hP.essentiallyLarge_top

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

Goal state before:
pp: case inl
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
h : D₁.W f✝
⊢ (D₁.P ⊔ D₂.P) i✝

pp: case inr
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
h : D₂.W f✝
⊢ (D₁.P ⊔ D₂.P) i✝

Tactic:
· exact Or.inl (D₁.src h)

Goal state after:
case inr
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
h : D₂.W f✝
⊢ (D₁.P ⊔ D₂.P) i✝
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_2.h₀
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
d : D₁ W Z
hf : toStep W Z ≫ fromStep W Z ≫ f = 𝟙 Z
⊢ Sigma.ι D₁.obj₁ d ≫
      D₁.l W Z ≫
        pushout.inr (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toStep W Z =
    (↑d.fst).hom ≫ Sigma.ι D₁.obj₂ d ≫ pushout.inl (D₁.t W Z) (D₁.l W Z)

Tactic:
reassoc_of% hf,

Goal state after:
case refine_2.h₀
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
d : D₁ W Z
hf : toStep W Z ≫ fromStep W Z ≫ f = 𝟙 Z
⊢ Sigma.ι D₁.obj₁ d ≫ D₁.l W Z ≫ toStep W Z = (↑d.fst).hom ≫ Sigma.ι D₁.obj₂ d ≫ pushout.inl (D₁.t W Z) (D₁.l W Z)
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: case isSuccLimit
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : Order.IsSuccLimit j
hj' : ∀ b < j, HasCardinalLT (↑(transfiniteIterate (φ Y m) b A)) κ₂
⊢ HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂

Tactic:
rw [transfiniteIterate_limit _ _ _ hj, Set.iSup_eq_iUnion]

Goal state after:
case isSuccLimit
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : Order.IsSuccLimit j
hj' : ∀ b < j, HasCardinalLT (↑(transfiniteIterate (φ Y m) b A)) κ₂
⊢ HasCardinalLT (↑(⋃ x, transfiniteIterate (φ Y m) (↑x) A)) κ₂
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : Presieve.ofArrows (fun x ↦ Y) (fun x ↦ π) g
hf : h ≫ g = f
⊢ Sieve.pullback g (Sieve.generate (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π)) ∈ (regularTopology C).sieves Y₁

Tactic:
apply regularTopology.mem_sieves_of_hasEffectiveEpi

Goal state after:
case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : Presieve.ofArrows (fun x ↦ Y) (fun x ↦ π) g
hf : h ≫ g = f
⊢ ∃ Y_1 π_1,
    EffectiveEpi π_1 ∧ (Sieve.pullback g (Sieve.generate (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π))).arrows π_1
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
x✝¹ : C
x✝ : x✝¹ ⟶ X
hh : Presieve.ofArrows Y π x✝
⊢ S.arrows x✝

Tactic:
by cases hh; exact h' _

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

Goal state before:
pp: case mpr
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
a✝ : Epi φ
data : (locallySurjective J A).MapFactorizationData (locallyInjective J A) φ :=
  (locallySurjective J A).factorizationData (locallyInjective J A) φ
this✝ : IsLocallySurjective data.i
this : IsLocallyInjective data.p
⊢ IsLocallySurjective φ

Tactic:
have : Epi data.p := epi_of_epi_fac data.fac

Goal state after:
case mpr
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
a✝ : Epi φ
data : (locallySurjective J A).MapFactorizationData (locallyInjective J A) φ :=
  (locallySurjective J A).factorizationData (locallyInjective J A) φ
this✝¹ : IsLocallySurjective data.i
this✝ : IsLocallyInjective data.p
this : Epi data.p
⊢ IsLocallySurjective φ
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝ : OneCochain G U
⊢ x✝ * 1 = x✝

Tactic:
ext; apply mul_one

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: case refine_1
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, Nonempty ((functor p).obj c ⟶ d)

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⟩
    obtain ⟨U, f, rfl⟩ := fiberMk_jointly_surjective x
    exact ⟨U, f, by simp⟩

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
⊢ ∀ {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'
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
hS : S ∈ J X
F' : Cᵒᵖ ⥤ Type (max u v) := FunctorToTypes.shrink.{max u v, w, v, u} F
e : (X : C) → F.obj (Opposite.op X) ≃ F'.obj (Opposite.op X) := fun X ↦ equivShrink (F.obj (Opposite.op X))
⊢ Presieve.IsSheafFor F S.arrows

Tactic:
have he (X Y : C) (f : X ⟶ Y) (x : F.obj (.op Y)) :
      (e X) (F.map f.op x) = F'.map f.op (e Y x) := by
    simp [e, F']

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
F' : Cᵒᵖ ⥤ Type (max u v) := FunctorToTypes.shrink.{max u v, w, v, u} F
e : (X : C) → F.obj (Opposite.op X) ≃ F'.obj (Opposite.op X) := fun X ↦ equivShrink (F.obj (Opposite.op X))
he :
  ∀ (X Y : C) (f : X ⟶ Y) (x : F.obj (Opposite.op Y)),
    (e X) ((ConcreteCategory.hom (F.map f.op)) x) = (ConcreteCategory.hom (F'.map f.op)) ((e Y) 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 : Coverage C
⊢ K.toPrecoverage ≤ K.toGrothendieck.toPrecoverage

Tactic:
← Precoverage.toGrothendieck_le_iff_le_toPrecoverage,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Coverage C
⊢ K.toGrothendieck ≤ K.toGrothendieck
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'
⊢ Mono S.ι

Tactic:
by
  suffices ∀ (X : C), Mono (S.ι.app X) from NatTrans.mono_of_mono_app _
  intro X
  exact ConcreteCategory.mono_of_injective _ Subtype.val_injective

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
M N : ↑(F.obj { as := op S })
φ : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun i ↦ Over.homMk (f i) ⋯)
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ (F.map f₁.op.toLoc).toFunctor.map (↑φ i₁) ≫ ((F.toDescentData f).obj N).hom q f₁ f₂ ⋯ ⋯ =
    ((F.toDescentData f).obj M).hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (↑φ i₂)

Tactic:
have := φ.property i₁ i₂ (Over.mk q) (Over.homMk f₁) (Over.homMk f₂) (by cat_disch)

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
M N : ↑(F.obj { as := op S })
φ : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun i ↦ Over.homMk (f i) ⋯)
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
this :
  (ConcreteCategory.hom ((F.presheafHom M N).map (Over.homMk f₁ ⋯).op)) (↑φ i₁) =
    (ConcreteCategory.hom ((F.presheafHom M N).map (Over.homMk f₂ ⋯).op)) (↑φ i₂)
⊢ (F.map f₁.op.toLoc).toFunctor.map (↑φ i₁) ≫ ((F.toDescentData f).obj N).hom q f₁ f₂ ⋯ ⋯ =
    ((F.toDescentData f).obj M).hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (↑φ i₂)
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ ∀ (x₂ : (fun X ↦ X) (G.obj X)) (x₃ : (fun X ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X)),
    (ConcreteCategory.hom ((χ m).app X)) x₂ = (ConcreteCategory.hom ((truth C).app X)) x₃ →
      ∃ x₁,
        (ConcreteCategory.hom (m.app X)) x₁ = x₂ ∧
          (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ = x₃

Tactic:
simp only [Functor.const_obj_obj, Functor.sieves_obj, χ_app, Opposite.op_unop,
      TypeCat.hom_ofHom, TypeCat.Fun.coe_mk, truth_app, Functor.isTerminalConst_from_app,
      Types.isTerminalPUnit_from_apply, and_true, forall_const]
    intro p hp
    simpa [eq_comm] using! congr($(hp).arrows (𝟙 _))

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
a : ℤ
⊢ P.triangEnvelope ≤ P.triangEnvelope.shift a

Tactic:
by
    intro X hX
    rw [prop_triangEnvelope_iff] at hX
    obtain ⟨n, hn⟩ := hX
    rw [prop_shift_iff, prop_triangEnvelope_iff]
    exact ⟨n, IsStableUnderShiftBy.le_shift _ hn⟩

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
h : P.IsStrongTriangulatedGenerator
⊢ P.IsClassicalTriangulatedGenerator

Tactic:
obtain ⟨n, hn⟩ := h
  rw [isClassicalTriangulatedGenerator_iff, eq_top_iff]
  exact hn ▸ (P.triangEnvelopeIter_le_triangEnvelope n)

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₃
P✝ : C
φ : P✝ ⟶ Z
hφ : φ ≫ (adj.homEquiv Z T.obj₃) h = 0
⊢ φ ≫ (Triangle.mk (G.map T.mor₁) f g).mor₃ = 0

Tactic:
by
        dsimp
        simp only [homEquiv_unit, Functor.comp_obj] at hφ
        rw [← cancel_mono ((G.commShiftIso (1 : ℤ)).inv.app T.obj₁), assoc, h₂', zero_comp,
          homEquiv_unit, assoc, reassoc_of% hφ, zero_comp]

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
⊢ ∀ {X Y : (Triangle C)ᵒᵖ} (f : X ⟶ Y),
    (F.mapTriangle.op ⋙ (triangleOpEquivalence D).functor).map f ≫
        (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop Y)).hom =
      (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop X)).hom ≫
        ((triangleOpEquivalence C).functor ⋙ F.op.mapTriangle).map f

Tactic:
by intros; ext <;> dsimp <;> simp only [id_comp, comp_id]

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
t : TStructure C
H : Type u'
inst✝² : Category.{v', u'} H
inst✝¹ : Preadditive H
inst✝ : t.Heart H
X : H
⊢ t.heart (t.ιHeart.obj X)

Tactic:
← t.essImage_ιHeart H

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
t : TStructure C
H : Type u'
inst✝² : Category.{v', u'} H
inst✝¹ : Preadditive H
inst✝ : t.Heart H
X : H
⊢ t.ιHeart.essImage (t.ιHeart.obj X)
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₁ : B ⟶ X₁
hx₁ : x₁ ≫ f₁ = 0
k' : (shiftFunctor C 1).obj (ι.obj B) ⟶ (shiftFunctor C 1).obj (ι.obj K)
hk' : (shiftFunctor C 1).map (ι.map x₁) = k' ≫ α ≫ f₃
⊢ k' ≫ (shiftFunctor C 1).map (ι.map (ιK f₃ α)) = (ι ⋙ shiftFunctor C 1).map x₁

Tactic:
shift_ι_map_ιK,

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
x₁ : B ⟶ X₁
hx₁ : x₁ ≫ f₁ = 0
k' : (shiftFunctor C 1).obj (ι.obj B) ⟶ (shiftFunctor C 1).obj (ι.obj K)
hk' : (shiftFunctor C 1).map (ι.map x₁) = k' ≫ α ≫ f₃
⊢ k' ≫ α ≫ f₃ = (ι ⋙ shiftFunctor C 1).map x₁
Module: Mathlib.CategoryTheory.Triangulated.WeakKernels

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ Nonempty (WeakLimitCone (parallelPair f 0))

Tactic:
obtain ⟨K, i, p, h⟩ := distinguished_cocone_triangle₁ f
    exact ⟨_, isWeakLimitKernelForkOfDistTriangle _ h⟩

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

Goal state before:
pp: case coe.coe
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a b : ℤ
f : WithBotTop.coe a ⟶ WithBotTop.coe b
⊢ WithBotTop.rec 0 t.truncLT (𝟭 C) (WithBotTop.coe a) ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) (WithBotTop.coe b)

Tactic:
exact t.natTransTruncLTOfLE a b (by simpa using leOfHom f)

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

Goal state before:
pp: case refine_2
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
⊢ A ⊆ ↑(F₁ • F₂) • C

Tactic:
calc
      A ⊆ (F₁ : Set M) • B := hFAB
      _ ⊆ (F₁ : Set M) • (F₂ : Set N) • C := by gcongr
      _ = (↑(F₁ • F₂) : Set N) • C := by simp

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

Goal state before:
pp: case pos
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
⊢ a ∈ F * (B / B)

pp: case neg
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
⊢ a ∈ F * (B / B)

Tactic:
· exact subset_mul_left _ hB.one_mem_div hau

Goal state after:
case neg
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
⊢ a ∈ F * (B / B)