mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : P.ContainsZero
n m n✝ : ℕ
hmn✝ : n ≤ n✝
a✝ : P.extensionProductIter n ≤ P.extensionProductIter n✝
⊢ P.extensionProductIter n ≤ P.extensionProductIter (n✝ + 1)

Tactic:
case succ n m hnm h =>
    refine le_trans h ?_
    rw [extensionProductIter_succ]
    exact le_extensionProduct_right P

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

Goal state before:
pp: case zero
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 Q : ObjectProperty C
inst✝ : Q.IsTriangulatedClosed₂
h : P ≤ Q
⊢ P ≤ Q.isoClosure

Tactic:
exact h.trans Q.le_isoClosure

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 L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
inst✝ : QuasiIso φ
⊢ QuasiIso ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).map φ)

Tactic:
rw [quasiIso_shift_iff]
  infer_instance

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

Goal state before:
pp: case left
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ c'.Rel (c'.prev (e.f j)) (e.f j)

pp: case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ ∀ (i : ι), ¬c'.Rel (e.f i) (e.f j)

Tactic:
· simpa only [c'.prev_eq' hj] using hj

Goal state after:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ ∀ (i : ι), ¬c'.Rel (e.f i) (e.f j)
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
i : ι
hi : c'.Rel (e.f i) (e.f j)
⊢ False

Tactic:
apply hi' i

Goal state after:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
i : ι
hi : c'.Rel (e.f i) (e.f j)
⊢ e.f i = i'
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]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hk : c.Rel j k
⊢ ¬(c'.Rel (c'.prev (e.f k)) (e.f k) ∧ ∀ (i : ι), ¬c'.Rel (e.f i) (e.f k))
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 L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
⊢ (Fork.ι cone ≫ (K.extendXIso e hj').inv) ≫ (K.extend e).d j' k' = 0

Tactic:
rw [assoc, ← comp_d_eq_zero_iff K e hj' hk hk' cone.ι, cone.condition]

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'
i : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryGE i
⊢ K.X (e.f i) = K.X i'

Tactic:
subst hi'

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
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'
i : ι
hi : ¬e.BoundaryGE i
⊢ K.X (e.f i) = K.X (e.f i)
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'
i : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
⊢ K.opcycles (e.f i) = K.opcycles i'

Tactic:
subst hi'

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
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'
i : ι
hi : e.BoundaryGE i
⊢ K.opcycles (e.f i) = K.opcycles (e.f i)
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'
i : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
⊢ K.pOpcycles (e.f i) ≫ (K.truncGE'XIsoOpcycles e ⋯ hi).inv =
    (K.restrictionXIso e hi').hom ≫ K.pOpcycles i' ≫ (K.truncGE'XIsoOpcycles e hi' hi).inv

Tactic:
subst hi'

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : e.BoundaryGE i
⊢ K.pOpcycles (e.f i) ≫ (K.truncGE'XIsoOpcycles e ⋯ hi).inv =
    (K.restrictionXIso e ⋯).hom ≫ K.pOpcycles (e.f i) ≫ (K.truncGE'XIsoOpcycles e ⋯ hi).inv
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'
i : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryGE i
⊢ (K.truncGE'XIso e ⋯ hi).inv = (K.restrictionXIso e hi').hom ≫ (K.truncGE'XIso e hi' hi).inv

Tactic:
subst hi'

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ (K.truncGE'XIso e ⋯ hi).inv = (K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ hi).inv
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.homologyπ j ≫ (K.extendHomologyIso e hj').inv = (K.extendCyclesIso e hj').inv ≫ (K.extend e).homologyπ j'

Tactic:
by
  simp only [← cancel_mono (K.extendHomologyIso e hj').hom,
    assoc, Iso.inv_hom_id, comp_id, homologyπ_extendHomologyIso_hom, Iso.inv_hom_id_assoc]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
A B : C
f : (singleFunctor C n).obj A ⟶ (singleFunctor C n).obj B
⊢ ∃ a, (singleFunctor C n).map a = f

Tactic:
by
    change Q.obj ((CochainComplex.singleFunctor C n).obj A) ⟶
      Q.obj ((CochainComplex.singleFunctor C n).obj B) at f
    suffices ∃ f', f = Q.map f' by
      obtain ⟨f', rfl⟩ := this
      obtain ⟨g, rfl⟩ := (CochainComplex.singleFunctor C n).map_surjective f'
      exact ⟨g, rfl⟩
    obtain ⟨X, _, _, s, _, g, rfl⟩ := right_fac_of_isStrictlyLE_of_isStrictlyGE n n f
    obtain ⟨A₀, ⟨e⟩⟩ := X.exists_iso_single n
    have ⟨φ, hφ⟩ := (CochainComplex.singleFunctor C n).map_surjective (e.inv ≫ s)
    have : IsIso ((singleFunctor C n).map φ) := by
      change IsIso (Q.map ((CochainComplex.singleFunctor C n).map φ))
      rw [hφ, Functor.map_comp]
      infer_instance
    have : IsIso φ := (NatIso.isIso_map_iff (singleFunctorCompHomologyFunctorIso C n) φ).1
        (by dsimp; infer_instance)
    have : IsIso (e.inv ≫ s) := by rw [← hφ]; infer_instance
    have : IsIso s := IsIso.of_isIso_comp_left e.inv s
    exact ⟨inv s ≫ g, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
W : MorphismProperty C
M : Type w'
inst✝¹⁰ : AddMonoid M
inst✝⁹ : HasShift C M
inst✝⁸ : W.IsCompatibleWithShift M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst✝⁷ : HasSmallLocalizedShiftedHom W M X Y
inst✝⁶ : HasSmallLocalizedShiftedHom W M X Z
inst✝⁵ : HasSmallLocalizedShiftedHom W M X T
inst✝⁴ : HasSmallLocalizedShiftedHom W M Y Z
inst✝³ : HasSmallLocalizedShiftedHom W M Y T
inst✝² : HasSmallLocalizedShiftedHom W M Z T
inst✝¹ : HasSmallLocalizedShiftedHom W M Z Z
inst✝ : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯

Tactic:
by
  apply (equiv W W.Q).injective
  simp only [equiv_comp, ShiftedHom.comp_assoc _ _ _ h₁₂ h₂₃ h]

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

Goal state before:
pp: case mpr.inr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
⊢ Small.{w, w'}
    ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
      (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))

Tactic:
· suffices Subsingleton ((Q.obj ((CochainComplex.singleFunctor C 0).obj X))⟦a⟧ ⟶
          (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))⟦b⟧) from inferInstance
      constructor
      intro x y
      rw [← cancel_mono ((Q.commShiftIso b).inv.app _),
        ← cancel_epi ((Q.commShiftIso a).hom.app _)]
      have : (((CochainComplex.singleFunctor C 0).obj X)⟦a⟧).IsStrictlyLE (-a) :=
        CochainComplex.isStrictlyLE_shift _ 0 _ _ (by lia)
      have : (((CochainComplex.singleFunctor C 0).obj Y)⟦b⟧).IsStrictlyGE (-b) :=
        CochainComplex.isStrictlyGE_shift _ 0 _ _ (by lia)
      apply (subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE _ _ (-a) (-b) (by
        lia)).elim

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

Tactic:
by
  change (shiftFunctorZero C B).inv.app X ≫ _ = _
  dsimp [Discrete.eqToHom, Discrete.addMonoidalFunctor_ε]
  congr 2
  apply eqToHom_map

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 : CompatibilityCounit adj e₁ e₂
X : C
⊢ e₁.hom.app X =
    F.map ((shiftFunctor C a).map (adj.unit.app X)) ≫
      F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app ((shiftFunctor D a).obj (F.obj X))

Tactic:
have := h (F.obj X)
  rw [← cancel_epi (F.map (e₂.inv.app _)), ← assoc, ← F.map_comp, Iso.inv_hom_id_app, F.map_id,
    id_comp] at this
  dsimp only [Functor.comp_obj, Functor.id_obj]
  rw [this, dsimp% e₁.hom.naturality_assoc, ← Functor.map_comp, left_triangle_components]
  simp only [Functor.map_id, comp_id]

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ᵒᵖ
⊢ (opShiftFunctorEquivalence C 0).unitIso.inv.app X =
    ((shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X).unop).op ≫
      ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op

Tactic:
by
  apply Quiver.Hom.unop_inj
  dsimp [opShiftFunctorEquivalence]
  rw [shiftFunctorZero_op_hom_app, unop_comp, Quiver.Hom.unop_op, Functor.map_comp,
    shiftFunctorCompIsoId_zero_zero_inv_app, assoc]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ (((((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
            (shiftFunctor C b).map
              ((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop) ≫
          (shiftFunctorAdd' C a b c ⋯).inv.app
            (Opposite.unop ((shiftFunctor Cᵒᵖ a).obj ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))))) ≫
        (shiftFunctor C c).map ((shiftFunctorAdd' Cᵒᵖ b a c ⋯).hom.app (Opposite.op X)).unop) ≫
      (shiftFunctor C c).map
        ((((shiftFunctorAdd' Cᵒᵖ b a c h).inv.app (Opposite.op X)).unop ≫ ((shiftFunctor Cᵒᵖ a).map g).unop) ≫
          Quiver.Hom.unop f) =
    (((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C b).map (Quiver.Hom.unop g)) ≫
      (shiftFunctor C b).map ((opEquiv a).symm f) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z

Tactic:
rw [assoc, assoc, assoc, assoc, ← Functor.map_comp, ← unop_comp_assoc,
    Iso.inv_hom_id_app]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app
            (Opposite.unop ((shiftFunctor Cᵒᵖ a).obj ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X)))) ≫
          (shiftFunctor C c).map
            ((𝟙 ((shiftFunctor Cᵒᵖ b ⋙ shiftFunctor Cᵒᵖ a).obj (Opposite.op X))).unop ≫
              ((shiftFunctor Cᵒᵖ a).map g).unop ≫ Quiver.Hom.unop f) =
    (((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C b).map (Quiver.Hom.unop g)) ≫
      (shiftFunctor C b).map ((opEquiv a).symm f) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z
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✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a b : A
h : a + b = 0
inst✝ : G.CommShift A
X : C
⊢ (iso adj a).hom.app X =
    F.map ((shiftFunctor C a).map (adj.unit.app X)) ≫
      F.map ((shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a b h).inv.app (F.obj X)))) ≫
        F.map ((shiftFunctor C a).map ((Functor.commShiftIso G b).hom.app ((shiftFunctor D a).obj (F.obj X)))) ≫
          F.map ((shiftFunctorCompIsoId C b a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X)))) ≫
            adj.counit.app ((shiftFunctor D a).obj (F.obj X))

Tactic:
obtain rfl : b = -a := eq_neg_of_add_eq_zero_right h
  simp [iso, iso', shiftEquiv']

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✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a b : A
h : a + b = 0
inst✝ : G.CommShift A
Y : C
⊢ (iso adj a).inv.app Y =
    (shiftFunctor D a).map (F.map ((shiftFunctorCompIsoId C a b h).inv.app Y)) ≫
      (shiftFunctor D a).map (F.map ((shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj Y)))) ≫
        (shiftFunctor D a).map (F.map ((Functor.commShiftIso G b).inv.app (F.obj ((shiftFunctor C a).obj Y)))) ≫
          (shiftFunctor D a).map (adj.counit.app ((shiftFunctor D b).obj (F.obj ((shiftFunctor C a).obj Y)))) ≫
            (shiftFunctorCompIsoId D b a ⋯).hom.app (F.obj ((shiftFunctor C a).obj Y))

Tactic:
obtain rfl : b = -a := eq_neg_of_add_eq_zero_right h
  simp [iso, iso', shiftEquiv']

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : (Triangle C)ᵒᵖ
φ : T₁ ⟶ T₂
⊢ (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₁).obj₁) ≫
      (shiftFunctor Cᵒᵖ 1).map ((Opposite.unop T₂).mor₃ ≫ (shiftFunctor C 1).map φ.unop.hom₁).op =
    φ.unop.hom₁.op ≫
      (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₂).obj₁) ≫
        (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₂).mor₃.op

Tactic:
op_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : (Triangle C)ᵒᵖ
φ : T₁ ⟶ T₂
⊢ (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₁).obj₁) ≫
      (shiftFunctor Cᵒᵖ 1).map (((shiftFunctor C 1).map φ.unop.hom₁).op ≫ (Opposite.unop T₂).mor₃.op) =
    φ.unop.hom₁.op ≫
      (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₂).obj₁) ≫
        (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₂).mor₃.op
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : Triangle Cᵒᵖ
φ : T₁ ⟶ T₂
⊢ ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map φ.hom₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop).op ≫
      (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁ =
    ((shiftFunctor C 1).map T₁.mor₃.unop).op ≫
      ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map φ.hom₁).unop).op ≫
        (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁

Tactic:
op_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : Triangle Cᵒᵖ
φ : T₁ ⟶ T₂
⊢ (((shiftFunctor C 1).map T₁.mor₃.unop).op ≫ ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map φ.hom₁).unop).op) ≫
      (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁ =
    ((shiftFunctor C 1).map T₁.mor₃.unop).op ≫
      ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map φ.hom₁).unop).op ≫
        (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁
Module: Mathlib.CategoryTheory.Triangulated.Yoneda

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
B : C
n a a' : ℤ
h : n + a = a'
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
x✝ : ↑((shiftFunctor Cᵒᵖ n ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj X✝)
⊢ (AddCommGrpCat.Hom.hom
        ((shiftFunctor Cᵒᵖ n ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).map f✝ ≫
          (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' n a a' h).symm;
              { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso.hom))
      x✝ =
    (AddCommGrpCat.Hom.hom
        ((let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' n a a' h).symm;
              { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso.hom ≫
          (preadditiveYoneda.obj ((shiftFunctor C a').obj B)).map f✝))
      x✝

Tactic:
apply ShiftedHom.opEquiv'_symm_comp _ _ _ h

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Linear

Goal state before:
pp: case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝ : Functor.Linear R (L ⋙ G)
this : L.EssSurj
X : D
r : R
⊢ G.map (r • 𝟙 X) = r • 𝟙 (G.obj X)

Tactic:
have e := L.objObjPreimageIso X

Goal state after:
case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝ : Functor.Linear R (L ⋙ G)
this : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
⊢ G.map (r • 𝟙 X) = r • 𝟙 (G.obj X)
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
x : relations.R →₀ A
⊢ solution.π (relations.map x) = 0

Tactic:
change solution.π.comp relations.map x = 0

Goal state after:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
x : relations.R →₀ A
⊢ (solution.π ∘ₗ relations.map) x = 0
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
⊢ Set.range relations.relation ⊆ ↑solution.π.ker

Tactic:
rintro _ ⟨r, rfl⟩

Goal state after:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
r : relations.R
⊢ relations.relation r ∈ ↑solution.π.ker
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Fintype n
⊢ M.SeparatingRight ↔ ∀ (v : n → R), M *ᵥ v = 0 → v = 0

Tactic:
have := Fintype.ofFinite m

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Fintype n
this : Fintype m
⊢ M.SeparatingRight ↔ ∀ (v : n → R), M *ᵥ v = 0 → v = 0
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Mᵀ.SeparatingLeft ↔ M.SeparatingRight

Tactic:
have := Fintype.ofFinite m

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Finite n
this : Fintype m
⊢ Mᵀ.SeparatingLeft ↔ M.SeparatingRight