mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Triangulated

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'
T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h
hT₃ : T₃ ∈ distinguishedTriangles
hβγσ : W (β.s ≫ γ.s ≫ σ)
ψ₃ : T₂.obj₃ ⟶ T₃.obj₃
hψ₃ : W ψ₃
hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s ≫ γ.s ≫ σ) ≫ T₃.mor₂
hψ₂ : T₂.mor₃ ≫ (shiftFunctor C 1).map α.s = ψ₃ ≫ T₃.mor₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ α.s (β.s ≫ γ.s ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (L.mapTriangle.map ψ)
⊢ (L.mapTriangle.map (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ α.f (γ.f ≫ σ) ⋯) ≫
        inv (L.mapTriangle.map ψ)).hom₁ =
    a

Tactic:
rw [← cancel_mono (L.mapTriangle.map ψ).hom₁, ← comp_hom₁, assoc, IsIso.inv_hom_id, comp_id]

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'
T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h
hT₃ : T₃ ∈ distinguishedTriangles
hβγσ : W (β.s ≫ γ.s ≫ σ)
ψ₃ : T₂.obj₃ ⟶ T₃.obj₃
hψ₃ : W ψ₃
hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s ≫ γ.s ≫ σ) ≫ T₃.mor₂
hψ₂ : T₂.mor₃ ≫ (shiftFunctor C 1).map α.s = ψ₃ ≫ T₃.mor₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ α.s (β.s ≫ γ.s ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (L.mapTriangle.map ψ)
⊢ (L.mapTriangle.map (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ α.f (γ.f ≫ σ) ⋯)).hom₁ =
    a ≫ (L.mapTriangle.map ψ).hom₁
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

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
inst✝ : P.IsStableUnderShift ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
h : P T.obj₁
⊢ P.trW T.mor₂

Tactic:
by
  rw [trW_iff']
  exact ⟨_, _, _, hT, h⟩

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hf : f ≫ (n.negOnePow • K.d (i + n) (j + n)) = 0
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
⊢ (f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n) = 0

Tactic:
simp only [Linear.comp_units_smul] at hf

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
hf : n.negOnePow • f ≫ K.d (i + n) (j + n) = 0
⊢ (f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n) = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
⊢ (singleFunctor C n).Additive

Tactic:
dsimp [singleFunctor, singleFunctors]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
⊢ ((HomotopyCategory.singleFunctors C).functor n ⋙ Qh).Additive
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + -1 = q
⊢ (fst φ).f p ≫ (inl φ).v p p ⋯ + (snd φ).v p q hpq ≫ (↑(inr φ)).v q p ⋯ = 𝟙 ((mappingCocone φ).X p)

Tactic:
by
  obtain rfl : q = p + -1 := by lia
  simp [fst, inl, snd, inr, mappingCocone,
    Cochain.leftShift_v (n := 1) _ _ _ _ _ p _ (p + -1) (by lia),
    Cochain.rightShift_v _ _ _ _ _ _ _ _ hpq,
    Cochain.leftShift_v _ _ _ _ _ _ _ _ (add_zero (p + -1)),
    Cochain.rightShift_v _ _ _ _ _ _ _ _ (add_zero (p + -1)),
    Int.negOnePow_even 2 ⟨1, rfl⟩,
    mappingCone.id_X φ (p + -1) p (by lia)]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : DerivedCategory C
f : K ⟶ L
⊢ IsIso f ↔ ∀ (n : ℤ), IsIso ((homologyFunctor C n).map f)

Tactic:
refine ⟨fun hf n ↦ inferInstance, fun hf ↦ ?_⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : DerivedCategory C
f : K ⟶ L
hf : ∀ (n : ℤ), IsIso ((homologyFunctor C n).map f)
⊢ IsIso f
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

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
D : Type u_2
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasZeroObject D
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁶ : Pretriangulated D
E : Type u_3
inst✝⁵ : Category.{v_3, u_3} E
inst✝⁴ : HasShift E ℤ
P : ObjectProperty C
inst✝³ : P.IsTriangulated
F : C ⥤ D
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : F.Full
T : Triangle D
hT : T ∈ distinguishedTriangles
X₁ : C
e₁ : F.obj X₁ ≅ T.obj₁
X₃ : C
e₃ : F.obj X₃ ≅ T.obj₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hh : F.map h = e₃.hom ≫ T.mor₃ ≫ (shiftFunctor D 1).map e₁.inv ≫ (Functor.commShiftIso F 1).inv.app X₁
X₂ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
H : Triangle.mk f g h ∈ distinguishedTriangles
⊢ F.essImage T.obj₂

Tactic:
exact ⟨X₂, ⟨Triangle.π₂.mapIso
      (isoTriangleOfIso₁₃ _ _ (F.map_distinguished _ H) hT e₁ e₃
        (by simp [hh, ← Functor.map_comp]))⟩⟩

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hk : c.Rel j k
⊢ ¬e.BoundaryGE k

Tactic:
dsimp [BoundaryGE]
  simp only [not_and, not_forall, not_not]
  intro
  exact ⟨j, by simpa only [e.rel_iff] using hk⟩

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : e.BoundaryGE i
⊢ (truncGE'Map (𝟙 K) e).f i = (𝟙 (K.truncGE' e)).f i

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ (truncGE'Map (𝟙 K) e).f i = (𝟙 (K.truncGE' e)).f i

Tactic:
· simp [truncGE'Map_f_eq_opcyclesMap _ _ hi rfl]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ (truncGE'Map (𝟙 K) e).f i = (𝟙 (K.truncGE' e)).f i
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.sc j).pOpcycles =
    (K.extendXIso e hj').inv ≫
      ((K.extend e).sc j').pOpcycles ≫
        (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).right.opcyclesIso.hom ≫
          (K.sc j).homologyData.right.opcyclesIso.inv

Tactic:
ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.sc j).pOpcycles =
    (K.extendXIso e hj').inv ≫
      (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).right.p ≫ (K.sc j).homologyData.right.opcyclesIso.inv
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsLE p
⊢ K.IsLE q

Tactic:
by
  rw [isLE_iff]
  intro i hi
  exact K.exactAt_of_isLE p _

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
X' : CochainComplex C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
this : IsIso (Q.map (CochainComplex.truncGEMap s a))
⊢ ∃ X',
    ∃ (_ : X'.IsStrictlyGE a) (_ : X'.IsStrictlyLE b), ∃ s, ∃ (x : IsIso (Q.map s)), ∃ g, f = inv (Q.map s) ≫ Q.map g

Tactic:
refine ⟨X'.truncGE a, inferInstance, inferInstance,
    CochainComplex.truncGEMap s a ≫ inv (X.πTruncGE a), ?_,
      CochainComplex.truncGEMap g a ≫ inv (Y.πTruncGE a), ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
X' : CochainComplex C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
this : IsIso (Q.map (CochainComplex.truncGEMap s a))
⊢ IsIso (Q.map (CochainComplex.truncGEMap s a ≫ inv (X.πTruncGE a)))

case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
X' : CochainComplex C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
this : IsIso (Q.map (CochainComplex.truncGEMap s a))
⊢ f =
    inv (Q.map (CochainComplex.truncGEMap s a ≫ inv (X.πTruncGE a))) ≫
      Q.map (CochainComplex.truncGEMap g a ≫ inv (Y.πTruncGE a))
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
h : HasSmallLocalizedHom W X Y
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
exact small_map (homEquiv W W.Q L).symm

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
⊢ AddCommGrpCat.ofHom ((Ext.mk₀ (f ≫ f')).postcomp X ⋯) =
    AddCommGrpCat.ofHom ((Ext.mk₀ f).postcomp X ⋯) ≫ AddCommGrpCat.ofHom ((Ext.mk₀ f').postcomp X ⋯)

Tactic:
ext α
    dsimp [AddCommGrpCat.ofHom]
    rw [← Ext.mk₀_comp_mk₀]
    symm
    apply Ext.comp_assoc
    lia

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (φ.app 0)
h₁ : IsIso (φ.app 1)
h₃ : IsIso (φ.app 3)
h₄ : Mono (φ.app 4)
⊢ Mono (app' φ 2 ⋯)

Tactic:
apply mono_of_epi_of_mono_of_mono (δlastFunctor.map φ) (R₁.exact_iff_δlast.1 hR₁).1
      (R₂.exact_iff_δlast.1 hR₂).1 <;> dsimp

Goal state after:
case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (φ.app 0)
h₁ : IsIso (φ.app 1)
h₃ : IsIso (φ.app 3)
h₄ : Mono (φ.app 4)
⊢ Epi (φ.app 0)

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (φ.app 0)
h₁ : IsIso (φ.app 1)
h₃ : IsIso (φ.app 3)
h₄ : Mono (φ.app 4)
⊢ Mono (φ.app 1)

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (φ.app 0)
h₁ : IsIso (φ.app 1)
h₃ : IsIso (φ.app 3)
h₄ : Mono (φ.app 4)
⊢ Mono (φ.app 3)
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (φ.app 0)
h₁ : IsIso (φ.app 1)
h₃ : IsIso (φ.app 3)
h₄ : Mono (φ.app 4)
this : Mono (app' φ 2 ⋯)
⊢ Epi (app' φ 2 ⋯)

Tactic:
apply epi_of_epi_of_epi_of_mono (δ₀Functor.map φ) (R₁.exact_iff_δ₀.1 hR₁).2
      (R₂.exact_iff_δ₀.1 hR₂).2 <;> dsimp <;> infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
⊢ φ 0 = 0

Tactic:
by rw [map_zero]

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
x✝ : PullbackShift C φ
⊢ φ 0 = 0

Tactic:
by rw [map_zero]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctorCompIsoId C 0 0 ⋯).inv.app (Opposite.unop X) ≫
      (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).hom.app X).unop =
    (shiftFunctorZero C ℤ).inv.app (Opposite.unop X) ≫
      (shiftFunctor C 0).map ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)) ≫
        (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).hom.app X).unop

Tactic:
shiftFunctorCompIsoId_zero_zero_inv_app,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X) ≫
        (shiftFunctor C 0).map ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X))) ≫
      (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).hom.app X).unop =
    (shiftFunctorZero C ℤ).inv.app (Opposite.unop X) ≫
      (shiftFunctor C 0).map ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)) ≫
        (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).hom.app X).unop
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ iCycles K i ≫ π.f i =
    cyclesMap π i ≫
      homologyπ ((singleFunctor C i).obj P) i ≫
        (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv

Tactic:
dsimp [singleFunctor, singleFunctors]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ iCycles K i ≫ π.f i =
    cyclesMap π i ≫
      homologyπ ((single C (ComplexShape.up ℤ) i).obj P) i ≫
        (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X Y : C
this : SMul R (X ⟶ Y) := smulOfRingMorphism φ X Y
a : X ⟶ Y
⊢ 0 • a = 0

Tactic:
simp only [smulOfRingMorphism_smul_eq, map_zero,
        zero_app, zero_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i =
    (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫
      (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyι ((singleFunctor C i).obj I) i ≫ opcyclesMap ι i

Tactic:
dsimp [singleFunctor, singleFunctors]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i =
    (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫
      (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫
        homologyι ((single C (ComplexShape.up ℤ) i).obj I) i ≫ opcyclesMap ι i
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i =
    (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫
      (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫
        homologyι ((single C (ComplexShape.up ℤ) i).obj I) i ≫ opcyclesMap ι i

Tactic:
rw [singleObjHomologySelfIso_inv_homologyι_assoc,
      ← pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, Iso.inv_hom_id_assoc, p_opcyclesMap]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
I : C
inst✝¹ : Injective I
K : CochainComplex C ℤ
i : ℤ
φ : Q.obj K ⟶ Q.obj ((CochainComplex.singleFunctor C i).obj I)
n : ℤ
hn : i < n
inst✝ : K.IsStrictlyGE n
⊢ φ = 0

Tactic:
obtain ⟨L, _, g, ι, h, rfl⟩ := left_fac_of_isStrictlyGE φ i
  have hπ : IsSplitMono ι := by
    rw [isIso_Q_map_iff_quasiIso] at h
    exact CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective ι
  have h₁ : inv (Q.map ι) = Q.map (retraction ι) := by
    rw [← cancel_epi (Q.map ι), IsIso.hom_inv_id, ← Q.map_comp, IsSplitMono.id, Q.map_id]
  have h₂ : g ≫ retraction ι = 0 := by
    apply HomologicalComplex.to_single_hom_ext
    apply (K.isZero_of_isStrictlyGE n i hn).eq_of_src
  rw [h₁, ← Q.map_comp, h₂, Q.map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : k = j
⊢ (e.repr (update v j x k)) i' = (e.repr x) i'

Tactic:
rw [h, update_self j x v]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ⇑f
⊢ IsCyclic G

Tactic:
classical
    cases nonempty_fintype G
    apply isCyclic_of_card_pow_eq_one_le
    intro n hn
    exact le_trans (card_nthRoots_subgroup_units f hf hn 1) (card_nthRoots n (f 1))

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
L : Type u_7
inst✝¹ : LeftCancelMonoid L
inst✝ : Finite L
⊢ Finite (L →* Rˣ)

Tactic:
let S := rootsOfUnity (Monoid.exponent L) R
  have : Finite (L →* S) := .of_injective _ DFunLike.coe_injective
  refine .of_surjective (fun f : L →* S ↦ (Subgroup.subtype _).comp f) fun f ↦ ?_
  have H a : f a ∈ S := by
    rw [mem_rootsOfUnity, ← map_pow, Monoid.pow_exponent_eq_one, map_one]
  exact ⟨.codRestrict f S H, MonoidHom.ext fun _ ↦ by simp⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
u : Rˣ
A : GL n R
⊢ ↑((scalar n) u) * ↑A = ↑A * ↑((scalar n) u)

Tactic:
coe_scalar,

Goal state after:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
u : Rˣ
A : GL n R
⊢ (Matrix.scalar n) ↑u * ↑A = ↑A * (Matrix.scalar n) ↑u
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : GL n R
⊢ (↑A).det * (↑A⁻¹).det = 1

Tactic:
← det_mul,

Goal state after:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : GL n R
⊢ (↑A * ↑A⁻¹).det = 1
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : GL n R
⊢ (↑A⁻¹).det * (↑A).det = 1

Tactic:
← det_mul,

Goal state after:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : GL n R
⊢ (↑A⁻¹ * ↑A).det = 1