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

Goal state before:
pp: case mp
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
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ → (φ.map L ⋯).op = (ψ.map L ⋯).op

pp: case mpr
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
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ (φ.map L ⋯).op = (ψ.map L ⋯).op → φ.map L ⋯ = ψ.map L ⋯

Tactic:
· apply Quiver.Hom.unop_inj

Goal state after:
case mpr
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
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ (φ.map L ⋯).op = (ψ.map L ⋯).op → φ.map L ⋯ = ψ.map L ⋯
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁷ : Category.{v_2, u_2} D
E : Type u_3
inst✝⁶ : Category.{v_3, u_3} E
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
inst✝² : HasShift E M
X Y : C
a : M
f : ShiftedHom X Y a
F : C ⥤ D
inst✝¹ : F.CommShift M
G : D ⥤ E
inst✝ : G.CommShift M
⊢ f.map (F ⋙ G) = (f.map F).map G

Tactic:
by
  simp [map, Functor.commShiftIso_comp_hom_app]

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

Goal state before:
pp: case succ
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✝ : IsTriangulated C
m m' : ℕ
h : m = m' + 1
n : ℕ
hn : P.extensionProductIter (n + m) = (P.extensionProductIter n).extensionProduct (P.extensionProductIter m')
⊢ P.extensionProductIter (n + (1 + m)) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')

Tactic:
add_comm 1 m,

Goal state after:
case succ
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✝ : IsTriangulated C
m m' : ℕ
h : m = m' + 1
n : ℕ
hn : P.extensionProductIter (n + m) = (P.extensionProductIter n).extensionProduct (P.extensionProductIter m')
⊢ P.extensionProductIter (n + (m + 1)) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ (shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K =
    (shortComplexFunctor C (up ℤ) a).map ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫
      (shiftShortComplexFunctorIso C n a a' ha').hom.app ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ≫
        (shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K

Tactic:
ext <;> dsimp

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ mn.negOnePow • (XIsoOfEq K ⋯).hom =
    ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K).f ((up ℤ).prev a) ≫
      (n.negOnePow • (XIsoOfEq ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ⋯).hom) ≫
        (m.negOnePow • (XIsoOfEq K ⋯).hom)

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ (XIsoOfEq K ⋯).hom =
    ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K).f a ≫
      (XIsoOfEq ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ⋯).hom ≫ (XIsoOfEq K ⋯).hom

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ mn.negOnePow • (XIsoOfEq K ⋯).hom =
    ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K).f ((up ℤ).next a) ≫
      (n.negOnePow • (XIsoOfEq ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ⋯).hom) ≫
        (m.negOnePow • (XIsoOfEq K ⋯).hom)
Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasZeroObject C
R : Type u_1
inst✝¹ : Ring R
n : ℤ
inst✝ : Linear R C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
r : R
⊢ { f := fun i ↦ if h : i = n then eqToHom ⋯ ≫ (r • f) ≫ eqToHom ⋯ else 0, comm' := ⋯ } =
    r • { f := fun i ↦ if h : i = n then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0, comm' := ⋯ }

Tactic:
aesop

Goal state after:
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✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
X Y : C
φ : P.trW.LeftFraction X Y
⊢ ∃ ψ, ψ.s ≫ φ.f = ψ.f ≫ φ.s

Tactic:
by
    obtain ⟨Z, f, g, H, mem⟩ := φ.hs
    obtain ⟨X', f', h', mem'⟩ := distinguished_cocone_triangle₁ (φ.f ≫ f)
    obtain ⟨a, ⟨ha₁, _⟩⟩ := complete_distinguished_triangle_morphism₁ _ _
      mem' H φ.f (𝟙 Z) (by simp)
    exact ⟨MorphismProperty.RightFraction.mk f' ⟨_, _, _, mem', mem⟩ a, ha₁⟩

Goal state after:
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 ∈ distinguishedTriangles, F.essImage T.obj₁ → F.essImage T.obj₃ → F.essImage T.obj₂

Tactic:
rintro T hT ⟨X₁, ⟨e₁⟩⟩ ⟨X₃, ⟨e₃⟩⟩
    have ⟨h, hh⟩ := F.map_surjective (e₃.hom ≫ T.mor₃ ≫ e₁.inv⟦1⟧' ≫
      (F.commShiftIso (1 : ℤ)).inv.app X₁)
    obtain ⟨X₂, f, g, H⟩ := distinguished_cocone_triangle₂ h
    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.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ (mappingConeCompHomotopyEquiv f g).hom ≫ (triangle (mappingConeCompTriangle f g).mor₁).mor₃ =
    (mappingConeCompTriangle f g).mor₃

Tactic:
by
  ext n
  simp [mappingConeCompHomotopyEquiv, MappingConeCompHomotopyEquiv.hom,
    lift_f _ _ _ _ _ (n + 1) rfl, ext_from_iff _ (n + 1) _ rfl]

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

Goal state before:
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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (φ ≫ φ') e).f i' = (extendMap φ e ≫ extendMap φ' e).f i'

Tactic:
simp [extendMap_f_eq_zero _ e i' (fun i hi => hi' ⟨i, hi⟩)]

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

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ x, c'.Rel (e.f j) (e.f x)
k : ι
hjk : k = j
hk : c.Rel j k
⊢ False

Tactic:
exact hjk' (by simpa only [hjk] using hk)

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

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
⊢ truncGEMap (𝟙 K) e = 𝟙 (K.truncGE e)

Tactic:
simp [truncGEMap, truncGE]

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

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
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncGE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : HasZeroObject C
⊢ truncGEMap (φ ≫ φ') e = truncGEMap φ e ≫ truncGEMap φ' e

Tactic:
simp [truncGEMap, truncGE]

Goal state after:
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.pOpcycles j ≫ (K.extendOpcyclesIso e hj').inv = (K.extendXIso e hj').inv ≫ (K.extend e).pOpcycles j'

Tactic:
← cancel_mono (K.extendOpcyclesIso e hj').hom,

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.pOpcycles j ≫ (K.extendOpcyclesIso e hj').inv) ≫ (K.extendOpcyclesIso e hj').hom =
    ((K.extendXIso e hj').inv ≫ (K.extend e).pOpcycles j') ≫ (K.extendOpcyclesIso e hj').hom
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ i < n, ExactAt K i) → K.IsGE n

Tactic:
intro h
    refine IsSupported.mk (fun i hi ↦ ?_)
    rw [notMem_range_embeddingUpIntGE_iff] at hi
    exact h i hi

Goal state after:
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 L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝ : HasZeroObject C
X : CochainComplex C ℕ
x✝¹ : ℤ
x✝ : ∀ (i : ℕ), (embeddingUpIntGE 0).f i ≠ x✝¹
⊢ ∀ (i : ℕ), embeddingUpNat.f i ≠ x✝¹

Tactic:
aesop

Goal state after:
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 L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝ : HasZeroObject C
X : ChainComplex C ℕ
x✝¹ : ℤ
x✝ : ∀ (i : ℕ), (embeddingUpIntLE 0).f i ≠ x✝¹
⊢ ∀ (i : ℕ), embeddingDownNat.f i ≠ x✝¹

Tactic:
aesop

Goal state after:
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 ℤ
inst✝² : HasZeroObject C
n : ℤ
inst✝¹ : K.IsStrictlyGE n
inst✝ : K.IsStrictlyLE n
⊢ mkHomFromSingle (𝟙 (K.X n)) ⋯ ≫ mkHomToSingle (𝟙 (K.X n)) ⋯ = 𝟙 ((single C (up ℤ) n).obj (K.X n))

Tactic:
aesop

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

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
this : IsIso (Q.map (CochainComplex.truncGEMap s n))
eq : Q.map (Y.πTruncGE n) ≫ Q.map (CochainComplex.truncGEMap s n) = Q.map s ≫ Q.map (Y'.πTruncGE n)
eq' : Q.map (X.πTruncGE n) ≫ Q.map (CochainComplex.truncGEMap g n) = Q.map g ≫ Q.map (Y'.πTruncGE n)
⊢ Q.map g ≫ inv (Q.map s) ≫ Q.map (Y.πTruncGE n) ≫ Q.map (CochainComplex.truncGEMap s n) =
    Q.map (X.πTruncGE n) ≫ Q.map (CochainComplex.truncGEMap g n)

Tactic:
simp only [eq, IsIso.inv_hom_id_assoc, eq']

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 Y Z T : C
n a b c : ℕ
h : a + b = c
⊢ ∀ (a_1 b_1 : Ext X Y a),
    AddMonoidHom.mk' (fun β ↦ (a_1 + b_1).comp β h) ⋯ =
      AddMonoidHom.mk' (fun β ↦ a_1.comp β h) ⋯ + AddMonoidHom.mk' (fun β ↦ b_1.comp β h) ⋯

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Shift.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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
⊢ CompatibilityCounit adj e₁ e₂

Tactic:
by
  intro Y
  have eq := h (G.obj Y)
  simp only [← cancel_mono (e₂.inv.app _ ≫ G.map (e₁.inv.app _)),
    assoc, Iso.hom_inv_id_app_assoc, comp_id, ← Functor.map_comp,
    Iso.hom_inv_id_app, Functor.comp_obj, Functor.map_id] at eq
  apply (adj.homEquiv _ _).injective
  dsimp
  rw [adj.homEquiv_unit, adj.homEquiv_unit, G.map_comp, adj.unit_naturality_assoc, ← eq]
  simp only [assoc, ← Functor.map_comp, Iso.inv_hom_id_app_assoc]
  erw [← e₂.inv.naturality]
  dsimp
  simp only [right_triangle_components, ← Functor.map_comp_assoc, Functor.map_id, id_comp,
    Iso.hom_inv_id_app, Functor.comp_obj]

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 φ
⊢ 𝟙 ((𝟭 (PullbackShift C φ)).obj X) =
    (shiftFunctorZero (PullbackShift C φ) A).inv.app X ≫
      (pullbackShiftIso C φ 0 0 ⋯).hom.app X ≫ (shiftFunctorZero C B).hom.app X

Tactic:
pullbackShiftFunctorZero_inv_app,

Goal state after:
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 φ
⊢ 𝟙 ((𝟭 (PullbackShift C φ)).obj X) =
    ((shiftFunctorZero C B).inv.app X ≫ (pullbackShiftIso C φ 0 0 ⋯).inv.app X) ≫
      (pullbackShiftIso C φ 0 0 ⋯).hom.app X ≫ (shiftFunctorZero C B).hom.app X
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ᵒᵖ
⊢ (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).inv.app X).unop ≫
      (shiftFunctorCompIsoId C 0 0 ⋯).hom.app (Opposite.unop X) =
    (shiftFunctor C 0).map
        (((shiftFunctorOpIso C 0 0 ⋯).inv.app X).unop ≫ ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op.unop) ≫
      (shiftFunctorZero C ℤ).hom.app (Opposite.unop X)

Tactic:
Quiver.Hom.unop_op,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).inv.app X).unop ≫
      (shiftFunctorCompIsoId C 0 0 ⋯).hom.app (Opposite.unop X) =
    (shiftFunctor C 0).map
        (((shiftFunctorOpIso C 0 0 ⋯).inv.app X).unop ≫ (shiftFunctorZero C ℤ).hom.app (Opposite.unop X)) ≫
      (shiftFunctorZero C ℤ).hom.app (Opposite.unop X)
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)).op.unop ≫ ((shiftFunctorOpIso C 0 0 ⋯).hom.app X).unop)

Tactic:
Quiver.Hom.unop_op,

Goal state after:
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) ≫ ((shiftFunctorOpIso C 0 0 ⋯).hom.app X).unop)
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
G✝ : C ⥤ D
inst✝³ : G✝.CommShift B
E : Type u_5
inst✝² : Category.{v_3, u_5} E
inst✝¹ : HasShift E B
G : D ⥤ E
inst✝ : G.CommShift B
x✝ : A
⊢ (commShiftIso (PullbackShift.functor φ (F ⋙ G)) x✝).hom ≫
      whiskerRight (PullbackShift.natIsoComp φ F G).hom (shiftFunctor (PullbackShift E φ) x✝) =
    (shiftFunctor (PullbackShift C φ) x✝).whiskerLeft (PullbackShift.natIsoComp φ F G).hom ≫
      (commShiftIso (PullbackShift.functor φ F ⋙ PullbackShift.functor φ G) x✝).hom

Tactic:
ext
    dsimp [PullbackShift.natIsoComp]
    simp only [commShiftPullback_iso_eq φ _ _ _ rfl, Iso.trans_hom, isoWhiskerRight_hom,
      isoWhiskerLeft_hom, Iso.symm_hom, comp_app, comp_obj, whiskerRight_app, Functor.comp_map,
      commShiftIso_comp_hom_app, whiskerLeft_app, assoc, map_id, comp_id, map_comp, id_comp]
    dsimp [PullbackShift.functor]
    slice_rhs 3 4 => rw [← G.map_comp, Iso.inv_hom_id_app]
    simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T₁ T₂ : Triangle Cᵒᵖ
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃
hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop
hc₂ :
  (shiftFunctor C 1).map T₂.mor₃.unop ≫ (shiftFunctor C 1).map c =
    ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫
      a.unop ≫ ((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop
⊢ (shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map a).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop =
    (shiftFunctor C 1).map T₂.mor₃.unop ≫ (shiftFunctor C 1).map c.op.unop

Tactic:
Quiver.Hom.unop_op,

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T₁ T₂ : Triangle Cᵒᵖ
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃
hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop
hc₂ :
  (shiftFunctor C 1).map T₂.mor₃.unop ≫ (shiftFunctor C 1).map c =
    ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫
      a.unop ≫ ((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop
⊢ (shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map a).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop =
    (shiftFunctor C 1).map T₂.mor₃.unop ≫ (shiftFunctor C 1).map c
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Goal state before:
pp: R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y Z : C
a b : ℕ
α : Ext X Y a
β : Ext Y Z b
c : ℕ
h : a + b = c
r : R
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α.comp (r • β) h = r • α.comp β h

Tactic:
aesop

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

Goal state before:
pp: R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y Z : C
a b : ℕ
α : Ext X Y a
β : Ext Y Z b
c : ℕ
h : a + b = c
r : R
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (r • α).comp β h = r • α.comp β h

Tactic:
aesop

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

Goal state before:
pp: R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y : C
r : R
f : X ⟶ Y
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ mk₀ (r • f) = r • mk₀ f

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasExt C
R : Type t
inst✝¹ : CommRing R
inst✝ : Linear R C
X Y Z : C
a b c : ℕ
h : a + b = c
⊢ ∀ (x y : Ext X Y a),
    { toFun := fun β ↦ (x + y).comp β h, map_add' := ⋯, map_smul' := ⋯ } =
      { toFun := fun β ↦ x.comp β h, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun β ↦ y.comp β h, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasExt C
R : Type t
inst✝¹ : CommRing R
inst✝ : Linear R C
X Y Z : C
a b c : ℕ
h : a + b = c
⊢ ∀ (m : R) (x : Ext X Y a),
    { toFun := fun β ↦ (m • x).comp β h, map_add' := ⋯, map_smul' := ⋯ } =
      (RingHom.id R) m • { toFun := fun β ↦ x.comp β h, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
M : ModuleCat R
⊢ M.projectiveShortComplex.ShortExact

Tactic:
by
  apply LinearMap.shortExact_shortComplexKer
  refine fun m ↦ ⟨Finsupp.single m 1, ?_⟩
  simp [Module.Basis.constr_apply]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝ : Ring A
relations : Relations A
⊢ relations.toQuotient ∘ₗ relations.map = 0

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ solution.π ∘ₗ relations.map = 0

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] N
r : relations.R
⊢ (Finsupp.linearCombination A fun g ↦ f (solution.var g)) = f ∘ₗ solution.π

Tactic:
aesop

Goal state after: