mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S]
    [inst_2 : InvolutiveInv ι] [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
    (∀ i ∈ s, 1 < f (v i)) →
      ∀ (i : ι),
        v i ≠ 1 →
          v i⁻¹ = (v i)⁻¹ → v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s) → v i ∈ closure (v '' s) → f (v i) ≠ 1
hi : v i ∉ closure (v '' s)
hi' : (v i)⁻¹ ∈ closure (v '' s)
⊢ v i⁻¹ ∈ closure (v '' s) ∨ (v i⁻¹)⁻¹ ∈ closure (v '' s)

Tactic:
left

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S]
    [inst_2 : InvolutiveInv ι] [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
    (∀ i ∈ s, 1 < f (v i)) →
      ∀ (i : ι),
        v i ≠ 1 →
          v i⁻¹ = (v i)⁻¹ → v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s) → v i ∈ closure (v '' s) → f (v i) ≠ 1
hi : v i ∉ closure (v '' s)
hi' : (v i)⁻¹ ∈ closure (v '' s)
⊢ v i⁻¹ ∈ closure (v '' s)
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case none
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
⊢ none = 0 ∨ ∃ r s, ∃ (hr : f r ≠ 0) (hs : f s ≠ 0), none = ↑(valueGroup.mk f r s hr hs)

Tactic:
left

Goal state after:
case none
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
⊢ none = 0
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : SimplexCategory
f g : ⦋0⦌ ⟶ n
h0 : (toOrderHom f) 0 = (toOrderHom g) 0
i : Fin (⦋0⦌.len + 1)
⊢ ↑((toOrderHom f) i) = ↑((toOrderHom g) i)

Tactic:
match i with | 0 => exact h0 ▸ rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i i' : Fin (l + 1)
hii' : i ≤ i'
⊢ (fun i ↦ ⟨↑i + j, ⋯⟩) i ≤ (fun i ↦ ⟨↑i + j, ⋯⟩) i'

Tactic:
by simpa only [Fin.mk_le_mk, add_le_add_iff_right] using! hii'

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
⊢ { X := P.X, p := 𝟙 P.X, idem := ⋯ }.p ≫ P.p ≫ P.p = P.p

Tactic:
by rw [coe_p, id_comp, P.idem]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ δ i.castSucc ≫ σ i = 𝟙 ⦋n⦌

Tactic:
δ_comp_σ_self

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ 𝟙 ⦋n⦌ = 𝟙 ⦋n⦌
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.castSucc = 𝟙 (X _⦋n⦌)

Tactic:
δ_comp_σ_self

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ 𝟙 (X _⦋n⦌) = 𝟙 (X _⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (CosimplicialObject C)

Tactic:
dsimp [CosimplicialObject]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (CosimplicialObject C)

Tactic:
dsimp [CosimplicialObject]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.castSucc ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
δ_comp_σ_self

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ 𝟙 (X ^⦋n⦌) = 𝟙 (X ^⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : n + j = m
hi'' : ↑i' = ↑i + j
⊢ X.δ i' ≫ X.δ₀Iter j ⋯ = X.δ₀Iter j ⋯ ≫ X.δ i

Tactic:
by
  dsimp [δ, δ₀Iter]
  simp only [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_δ' _ _ _ _ hi'']

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case inr
n : ℕ
k : Fin ⦋n + 1⦌.len
⊢ ↑((ConcreteCategory.hom (σ₀Iter 1 ⋯)) k.succ) = ↑((ConcreteCategory.hom (σ 0)) k.succ)

Tactic:
rw [σ₀Iter_coe_eq_of_ge .., coe_σ]

Goal state after:
case inr
n : ℕ
k : Fin ⦋n + 1⦌.len
⊢ ↑k.succ - 1 = ↑(Fin.predAbove 0 k.succ)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n✝ : ℕ
j : Fin (n✝ + 1)
⊢ (p.app (op ⦋n✝ + 1⦌) ≫ H.h j.succ) ≫ Y.δ j.castSucc.succ =
    (p.app (op ⦋n✝ + 1⦌) ≫ H.h j.castSucc) ≫ Y.δ j.castSucc.succ

Tactic:
by
    simpa using p.app _ ≫= H.h_succ_comp_δ_castSucc_succ j

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subfunctor F
⊢ x ∈ G.obj X → ofSection x ≤ G

Tactic:
· rintro hx U _ ⟨f, rfl⟩
    exact G.map f hx

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X.op _⦋n⦌
⊢ (∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), opObjEquiv x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))) ↔
    ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.op.map f.op))

Tactic:
refine exists_congr (fun m ↦ exists_congr (fun _ ↦ ?_))

Goal state after:
X : SSet
n : ℕ
x : X.op _⦋n⦌
m : ℕ
x✝ : m < n
⊢ (∃ f, ∃ (_ : Epi f), opObjEquiv x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))) ↔
    ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.op.map f.op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
⊢ Functor.Elements X → X.S

Tactic:
by rintro ⟨⟨⟨n⟩⟩, x⟩; exact S.mk x

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: n m : ℕ
inst✝ : NeZero n
hm : n ≤ m
⊢ (incl n m ⋯).Initial

Tactic:
by
  have : (incl n m hm ⋙ inclusion m).Initial :=
    Functor.initial_of_natIso (inclCompInclusion (by lia)).symm
  apply Functor.initial_of_comp_full_faithful _ (inclusion m)

Goal state after:
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝¹ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst✝ : CategoryWithHomology C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Even j
⊢ (alternatingConst A hOdd hEven hc).iCycles j ≫ φ = 0

Tactic:
rw [← cancel_epi (ShortComplex.cyclesMapIso
    (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)).inv]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝¹ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst✝ : CategoryWithHomology C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Even j
⊢ (ShortComplex.cyclesMapIso (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)).inv ≫
      (alternatingConst A hOdd hEven hc).iCycles j ≫ φ =
    (ShortComplex.cyclesMapIso (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)).inv ≫ 0
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Odd n
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) n

Tactic:
exact ⟨⟨alternatingConstHomologyDataOdd X _ h⟩⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case succ
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
m : ℕ
hm : #S = m + 1
⊢ (face S).toSSet.HasDimensionLT d

Tactic:
· rw [← hasDimensionLT_iff_of_iso
      (isoOfRepresentableBy (faceRepresentableBy S m (monoEquivOfFin S (by simpa))))]
    exact hasDimensionLT_of_le _ (m + 1) _

Goal state after:
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
⊢ c.ε 0 = 1

Tactic:
by
  apply map_one

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
inst✝⁴ : Category.{v_3, u_3} C₃
inst✝³ : Category.{v_4, u_4} C₄
inst✝² : Category.{v_5, u_5} C₁₂
inst✝¹ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
inst✝ :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₁ Y₁ : GradedObject I₁ C₁
φ✝ : X₁ ⟶ Y₁
X₂ : GradedObject I₂ C₂
X₃ Y₃ : GradedObject I₃ C₃
φ : X₃ ⟶ Y₃
j : J
i₁ : I₁
i₂ : I₂
i₃ : I₃
h : p (i₁, i₂, i₃) = j
⊢ ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ j ≫ mapTrifunctorMapMap F p φ✝ (𝟙 X₂) (𝟙 Y₃) j =
    ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      mapTrifunctorMapMap F p φ✝ (𝟙 X₂) (𝟙 X₃) j ≫ mapTrifunctorMapMap F p (𝟙 Y₁) (𝟙 X₂) φ j

Tactic:
simp only [ι_mapTrifunctorMapMap_assoc, categoryOfGradedObjects_id, Functor.map_id,
              NatTrans.id_app, ι_mapTrifunctorMapMap, id_comp, NatTrans.naturality_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Center.NegOnePow

Goal state before:
pp: case inr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X : C
n : ℤ
⊢ (↑((-1) ^ (2 * n + 1))).app X = (2 * n + 1).negOnePow • 𝟙 X

Tactic:
· rw [Int.negOnePow_odd _ (by exact odd_two_mul_add_one n)]
    simp [Units.smul_def, zpow_add, Int.two_mul, ← mul_zpow]

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: case pos
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₃ : c₁.Rel (c₁.prev i₁) i₁
⊢ c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
      (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j' =
    0

Tactic:
rw [ιMapBifunctorOrZero_eq_zero, comp_zero, comp_zero, smul_zero]
    intro h₄
    apply h
    rw [← h', ← h₄]
    exact ComplexShape.rel_π₁ c₂ c h₃ i₂

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (NatIso.ofComponents (fun X ↦ t.z (a + b) c • (shiftFunctorAdd C (a + b) c).app X) ⋯).hom.app X ≫
      (shiftFunctor C c).map ((NatIso.ofComponents (fun X ↦ t.z a b • (shiftFunctorAdd C a b).app X) ⋯).hom.app X) =
    eqToHom ⋯ ≫
      (NatIso.ofComponents (fun X ↦ t.z a (b + c) • (shiftFunctorAdd C a (b + c)).app X) ⋯).hom.app X ≫
        (NatIso.ofComponents (fun X ↦ t.z b c • (shiftFunctorAdd C b c).app X) ⋯).hom.app ((shiftFunctor C a).obj X)

Tactic:
by
    dsimp
    simp only [Functor.map_comp, Category.assoc, CatCenter.smul_iso_hom_eq]
    rw [CatCenter.naturality, CatCenter.naturality_assoc, CatCenter.naturality_assoc,
      CatCenter.naturality_assoc, CatCenter.naturality_assoc, CatCenter.naturality_assoc,
      t.shift_z_app, CatCenter.naturality, CatCenter.naturality_assoc,
      ← CatCenter.mul_app_assoc, ← CatCenter.mul_app_assoc,
      ← Units.val_mul, ← Units.val_mul, t.assoc a b c]
    simp [shiftFunctorAdd_assoc_hom_app (C := C) a b c X, shiftFunctorAdd']

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom

Goal state before:
pp: case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := ⋯
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (Cocycle.equivHomShift.symm y₁) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (Cocycle.equivHomShift.symm y₂)

Tactic:
← toHom_mk,

Goal state after:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
⊢ toHom (mk y₁) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (Cocycle.equivHomShift.symm y₂)
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i' : ι'
⊢ (extendMap f e).f i' = (dNext i') (extend.hom e h.hom) + (prevD i') (extend.hom e h.hom) + (extendMap g e).f i'

Tactic:
by_cases hi' : ∃ i, e.f i = i'
    · obtain ⟨i, rfl⟩ := hi'
      rw [extendMap_f _ _ rfl, extendMap_f _ _ rfl, h.comm i, Preadditive.add_comp,
        Preadditive.add_comp, Preadditive.comp_add, Preadditive.comp_add, add_left_inj]
      congr 1
      · by_cases hi : c.Rel i (c.next i)
        · have hi' : c'.Rel (e.f i) (e.f (c.next i)) := by rwa [e.rel_iff]
          simp [dNext_eq _ hi, dNext_eq _ hi', extend.hom_eq _ _ rfl rfl,
            extend_d_eq _ _ rfl rfl]
        · rw [dNext_eq_zero _ _ hi]
          by_cases hi' : c'.Rel (e.f i) (c'.next (e.f i))
          · simp [dNext_eq _ hi', K.extend_d_from_eq_zero _ _ _ _ rfl hi]
          · simp [dNext_eq_zero _ _ hi']
      · by_cases hi : c.Rel (c.prev i) i
        · have hi' : c'.Rel (e.f (c.prev i)) (e.f i) := by rwa [e.rel_iff]
          simp [prevD_eq _ hi, prevD_eq _ hi', extend.hom_eq _ _ rfl rfl,
            extend_d_eq _ _ rfl rfl]
        · rw [prevD_eq_zero _ _ hi]
          by_cases hi' : c'.Rel (c'.prev (e.f i)) (e.f i)
          · simp [prevD_eq _ hi', L.extend_d_to_eq_zero _ _ _ _ rfl hi]
          · simp [prevD_eq_zero _ _ hi']
    · exact (isZero_extend_X _ _ _ (by tauto)).eq_of_src _ _

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

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
t : TStructure C
n : ℤ
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : t.IsLE X✝ n
⊢ t.IsLE Y✝ n

Tactic:
exact t.isLE_of_iso e _

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

Goal state before:
pp: case mpr
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
X : C
n a n' : ℤ
hn' : a + n' = n
⊢ t.IsLE X n → t.IsLE ((shiftFunctor C a).obj X) n'

Tactic:
intro
    exact t.isLE_shift X n a n' hn'

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
A B : C
i : A ⟶ B
hi : coproducts.{w, v, u} T i
⊢ T.rlp.llp i

Tactic:
rw [coproducts_iff] at hi

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
A B : C
i : A ⟶ B
hi : ∃ J, T.colimitsOfShape (Discrete J) i
⊢ T.rlp.llp i
Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : CategoryWithWeakEquivalences C
⊢ WeakEquivalence f.op ↔ WeakEquivalence f

Tactic:
simp [weakEquivalence_iff, weakEquivalences_op]

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

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
X : C
a b : ℤ
hn : b ≤ a
⊢ t.IsGE ((t.truncGE a).obj X) b

Tactic:
have : t.IsGE ((t.truncGE a).obj X) a := by dsimp [truncGE]; infer_instance

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
X : C
a b : ℤ
hn : b ≤ a
this : t.IsGE ((t.truncGE a).obj X) a
⊢ t.IsGE ((t.truncGE a).obj X) b
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
hg₁ : epiWithInjectiveKernel g₁
hg₂ : epiWithInjectiveKernel g₂
⊢ epiWithInjectiveKernel (g₁ ≫ g₂)

Tactic:
rw [epiWithInjectiveKernel_iff] at hg₁ hg₂ ⊢
    obtain ⟨I₁, _, f₁, w₁, ⟨σ₁⟩⟩ := hg₁
    obtain ⟨I₂, _, f₂, w₂, ⟨σ₂⟩⟩ := hg₂
    refine ⟨I₁ ⊞ I₂, inferInstance, biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, ?_, ⟨?_⟩⟩
    · ext
      · simp [reassoc_of% w₁]
      · simp [reassoc_of% σ₁.s_g, w₂]
    · exact
        { r := σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr
          s := σ₂.s ≫ σ₁.s
          f_r := by
            ext
            · simp [σ₁.f_r]
            · simp [reassoc_of% w₁]
            · simp
            · simp [reassoc_of% σ₁.s_g, σ₂.f_r]
          s_g := by simp [reassoc_of% σ₁.s_g, σ₂.s_g]
          id := by
            dsimp
            have h := g₁ ≫= σ₂.id =≫ σ₁.s
            simp only [add_comp, assoc, comp_add, id_comp] at h
            rw [← σ₁.id, ← h]
            simp only [comp_add, add_comp, assoc, BinaryBicone.inl_fst_assoc,
              BinaryBicone.inr_fst_assoc, zero_comp, comp_zero, add_zero,
              BinaryBicone.inl_snd_assoc, BinaryBicone.inr_snd_assoc, zero_add]
            abel }

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

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
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsGE T.obj₁ n
h₃ : t.IsGE T.obj₃ n
⊢ t.IsGE T.obj₂ n

Tactic:
by
  rw [t.isGE_iff_orthogonal (n-1) n (by lia)]
  intro Y f hY
  obtain ⟨f', hf'⟩ := Triangle.coyoneda_exact₂ _ hT f (t.zero _ (n-1) n (by lia))
  rw [hf', t.zero f' (n-1) n (by lia), zero_comp]

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

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
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
⊢ IsIso ((t.truncGE n₁).map T.mor₂)

Tactic:
rw [isIso_truncGE_map_iff _ _ _ _ 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
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
⊢ ∃ X f h, ∃ (_ : Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) h ∈ distinguishedTriangles), t.IsLE X n₀
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n₀✝ n₁ : ℤ
hn₁ : n₀✝ + 1 = n₁
hf : ∀ i ≤ n₀✝, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
⊢ Mono (homologyMap (ι f n₁) n₁)

Tactic:
mono_homologyMap_iff_up_to_refinements _ n₀ n₁ (n₁ + 1) (by simp; lia) (by simp)

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n₀✝ n₁ : ℤ
hn₁ : n₀✝ + 1 = n₁
hf : ∀ i ≤ n₀✝, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
⊢ ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X n₁),
    x₂ ≫ K.d n₁ (n₁ + 1) = 0 →
      ∀ (y₁ : A ⟶ (mid K L n₁).X n₀),
        x₂ ≫ (ι f n₁).f n₁ = y₁ ≫ (mid K L n₁).d n₀ n₁ → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ K.d n₀ n₁
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n q : ℤ
hq : q < n
⊢ QuasiIsoAt (π f n) q

Tactic:
by
  have := mono_homologyMap_π f n q (by lia)
  have := epi_homologyMap_π f n q hq
  rw [quasiIsoAt_iff_isIso_homologyMap]
  apply Balanced.isIso_of_mono_of_epi

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : Mono f
T : ShortComplex C :=
  { X₁ := homology K n, X₂ := homology L n, X₃ := homology (cokernel f) n, f := homologyMap f n,
    g := homologyMap (cokernel.π f) n, zero := ⋯ }
⊢ 𝟙 T.X₂ ≫ (homologyShortComplex f n).g = T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n

Tactic:
by
        dsimp
        rw [Category.id_comp, ← homologyMap_comp, α]

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
E : C₂ ≌ C₃
E' : D₂ ≌ D₃
w' : H₂ ⋙ E'.functor ≅ E.functor ⋙ H₃
L₁₂ : C₁ ⥤ C₃
R₁₂ : D₁ ⥤ D₃
eL : L₁ ⋙ E.functor ≅ L₁₂
eR : R₁ ⋙ E'.functor ≅ R₁₂
⊢ (w.vComp' w'.hom eL eR).GuitartExact ↔ w.GuitartExact

Tactic:
rw [← vComp_iff_of_equivalences w E E' w', TwoSquare.vComp', whiskerVertical_iff]

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
inst✝¹ : EnoughInjectives C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
inst✝ : K.IsStrictlyGE n₁
⊢ ∃ L i, ∃ (_ : Mono i) (_ : QuasiIso i) (_ : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n₀

Tactic:
have : K.IsStrictlyGE (n₀ + 1) := by rw [h]; infer_instance
  obtain ⟨L, hL, i, p, hi, hi', hp, _⟩ := cm5a (0 : K ⟶ 0) n₀
  exact ⟨L, i, hi, hi', (degreewiseEpiWithInjectiveKernel_iff_of_isZero p
    (Limits.isZero_zero _)).1 hp, hL⟩

Goal state after: