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

Goal state before:
pp: C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝¹ : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝ : L₂.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
⊢ (homEquiv W L₁ L₂) (isoOfHom L₁ W f hf).inv = (isoOfHom L₂ W f hf).inv

Tactic:
rw [← cancel_mono (isoOfHom L₂ W f hf).hom, Iso.inv_hom_id, isoOfHom_hom,
    ← homEquiv_map W L₁ L₂ f, ← homEquiv_comp, isoOfHom_inv_hom_id, homEquiv_id]

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

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
hi : ¬∃ j, c.Rel i j
this✝ : Epi S₂.g
eq : homologyMap φ.τ₂ i ≫ homologyMap S₂.g i = homologyMap S₁.g i ≫ homologyMap φ.τ₃ i
this : Epi (homologyMap S₂.g i)
⊢ Epi (homologyMap φ.τ₃ i)

Tactic:
exact epi_of_epi_fac eq.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
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
e : Ext X Y n
⊢ homEquiv (chgUniv e) = homEquiv e

Tactic:
by
  apply SmallShiftedHom.equiv_chgUniv

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ᵒᵖ
⊢ 𝟙 ((shiftFunctor Cᵒᵖ 0).obj X) =
    (shiftFunctorOpIso C 0 0 ⋯).hom.app X ≫
      𝟙 (Opposite.op ((shiftFunctor C 0).obj (Opposite.unop X))) ≫ (shiftFunctorOpIso C 0 0 ⋯).inv.app X

Tactic:
id_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ 𝟙 ((shiftFunctor Cᵒᵖ 0).obj X) = (shiftFunctorOpIso C 0 0 ⋯).hom.app X ≫ (shiftFunctorOpIso C 0 0 ⋯).inv.app X
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
h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ (a₁ + a₂) ⋯).inv.app X =
    (pullbackShiftIso C φ a₂ (φ a₂) ⋯).hom.app ((shiftFunctor (PullbackShift C φ) a₁).obj X) ≫
      𝟙 ((shiftFunctor C (φ a₂)).obj ((shiftFunctor (PullbackShift C φ) a₁).obj X)) ≫
        (shiftFunctorAdd' C (φ a₁) (φ a₂) (φ a₁ + φ a₂) ⋯).inv.app X ≫
          (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv.app X

Tactic:
id_comp,

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 φ
a₁ a₂ : A
h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ (a₁ + a₂) ⋯).inv.app X =
    𝟙 ((shiftFunctor C (φ a₂)).obj ((shiftFunctor (PullbackShift C φ) a₁).obj X)) ≫
      (shiftFunctorAdd' C (φ a₁) (φ a₂) (φ a₁ + φ a₂) ⋯).inv.app X ≫
        (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv.app X
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
h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ (a₁ + a₂) ⋯).inv.app X =
    𝟙 ((shiftFunctor C (φ a₂)).obj ((shiftFunctor (PullbackShift C φ) a₁).obj X)) ≫
      (shiftFunctorAdd' C (φ a₁) (φ a₂) (φ a₁ + φ a₂) ⋯).inv.app X ≫
        (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv.app X

Tactic:
id_comp,

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 φ
a₁ a₂ : A
h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ (a₁ + a₂) ⋯).inv.app X =
    (shiftFunctorAdd' C (φ a₁) (φ a₂) (φ a₁ + φ a₂) ⋯).inv.app X ≫
      (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv.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ᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ a₃).obj X) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).1 (Opposite.unop X))) ≫
          𝟙 ((shiftFunctor Cᵒᵖ a₂).obj (Opposite.op ((shiftFunctor C b₁).1 (Opposite.unop X)))) ≫
            (shiftFunctorOpIso C a₂ b₂ h₂).hom.app ((shiftFunctor C b₁).op.obj X) ≫
              ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X

Tactic:
id_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ a₃).obj X) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).1 (Opposite.unop X))) ≫
          (shiftFunctorOpIso C a₂ b₂ h₂).hom.app ((shiftFunctor C b₁).op.obj X) ≫
            ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.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ᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ a₃).obj X) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      𝟙 (Opposite.op ((shiftFunctor C b₃).obj (Opposite.unop X))) ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X

Tactic:
id_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ a₃).obj X) = (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.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ᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op ≫
      (𝟙 ((shiftFunctor C p).obj (Opposite.unop ((shiftFunctor Cᵒᵖ p).obj X)))).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      (𝟙 ((shiftFunctor C n).obj (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctor C n).map
              (𝟙 ((shiftFunctor C m).obj (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))) ≫
                (shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctorAdd' C m n p h).hom.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
            ((shiftFunctor C p).map
                ((shiftFunctorOpIso C m (-m) ⋯).hom.app ((shiftFunctor Cᵒᵖ n).obj X) ≫
                    (𝟙 ((shiftFunctor C (-m)).obj (Opposite.unop ((shiftFunctor C (-n)).op.obj X)))).op ≫
                      ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)).op ≫
                        (shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).op

Tactic:
id_comp,

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

Tactic:
id_comp,

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

Tactic:
id_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op ≫
      (𝟙 ((shiftFunctor C p).obj (Opposite.unop ((shiftFunctor Cᵒᵖ p).obj X)))).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map
              ((𝟙 ((shiftFunctor C (-m)).obj (Opposite.unop ((shiftFunctor C (-n)).op.obj X)))).op ≫
                  ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)).op ≫
                    (shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).op
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
            (𝟙 (Opposite.unop ((shiftFunctor Cᵒᵖ a).obj ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X)))) ≫
              ((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:
id_comp,

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ᵒᵖ 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.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✝² x✝¹ : A
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
      F.map ((shiftFunctorAdd' (PullbackShift C φ) (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
        (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor (PullbackShift C φ) (φ x✝²)).obj x✝) ≫
          (shiftFunctor (PullbackShift D φ) (φ x✝¹)).map ((commShiftIso F (φ x✝²)).hom.app x✝) ≫
            (shiftFunctorAdd' (PullbackShift D φ) (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) ≫
              (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) =
    F.map ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
      F.map ((shiftFunctorAdd' C (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
        (((𝟙 (F.obj ((shiftFunctor C (φ x✝¹)).obj ((shiftFunctor C (φ x✝²)).obj x✝))) ≫
                (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor C (φ x✝²)).obj x✝)) ≫
              (shiftFunctor D (φ x✝¹)).map ((commShiftIso F (φ x✝²)).hom.app x✝)) ≫
            (shiftFunctorAdd' D (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝)) ≫
          (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝)

Tactic:
id_comp,

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 φ
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✝² x✝¹ : A
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
      F.map ((shiftFunctorAdd' (PullbackShift C φ) (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
        (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor (PullbackShift C φ) (φ x✝²)).obj x✝) ≫
          (shiftFunctor (PullbackShift D φ) (φ x✝¹)).map ((commShiftIso F (φ x✝²)).hom.app x✝) ≫
            (shiftFunctorAdd' (PullbackShift D φ) (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) ≫
              (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) =
    F.map ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
      F.map ((shiftFunctorAdd' C (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
        (((commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor C (φ x✝²)).obj x✝) ≫
              (shiftFunctor D (φ x✝¹)).map ((commShiftIso F (φ x✝²)).hom.app x✝)) ≫
            (shiftFunctorAdd' D (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝)) ≫
          (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

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

Tactic:
id_comp,

Goal state after:
case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ (opShiftFunctorEquivalence C 1).counitIso.inv.app T.obj₃ ≫
      (shiftFunctor Cᵒᵖ 1).map
        (((shiftFunctor C 1).map T.mor₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app T.obj₁) =
    T.mor₃
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
this : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
⊢ (singleObjXSelf (ComplexShape.up ℤ) i P).hom ≫ 𝟙 P ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv =
    𝟙 (((singleFunctor C i).obj P).X i)

Tactic:
id_comp,

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
this : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
⊢ (singleObjXSelf (ComplexShape.up ℤ) i P).hom ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv =
    𝟙 (((singleFunctor C i).obj P).X i)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯) ≫ AddCommGrpCat.ofHom (hS.extClass.postcomp X h) = 0

Tactic:
ext x
        dsimp
        simp only [comp_assoc_of_second_deg_zero, ShortComplex.ShortExact.comp_extClass,
          comp_zero]

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
this : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α
⊢ (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ 𝟙 I ≫ (singleObjXSelf (ComplexShape.up ℤ) i I).inv =
    𝟙 (((singleFunctor C i).obj I).X i)

Tactic:
id_comp,

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
this : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α
⊢ (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ (singleObjXSelf (ComplexShape.up ℤ) i I).inv =
    𝟙 (((singleFunctor C i).obj I).X i)
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Finite n
this : Fintype n
h : ∀ (v : m → R), v ᵥ* M = 0 → v = 0
w : m → R
hw : ∀ (w_1 : n → R), w ⬝ᵥ M *ᵥ w_1 = 0
i : n
⊢ (w ᵥ* M) i = 0 i

Tactic:
simpa using! hw <| Pi.single i 1

Goal state after:
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
this✝ : Fintype m
this : Fintype n
⊢ Mᵀ.SeparatingLeft ↔ M.SeparatingRight

Tactic:
simp_rw [separatingLeft_def, separatingRight_def, dotProduct_transpose_mulVec]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case calc_2
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
⊢ ∑ n ∈ range (orderOf x), ↑↑x ^ n = 0

Tactic:
rw [← mul_left_inj' hx1, zero_mul, geom_sum_mul]

Goal state after:
case calc_2
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
⊢ ↑↑x ^ orderOf x - 1 = 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

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

Tactic:
rw [det_mul, A.prop, B.prop, one_mul]

Goal state after:
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : R
⊢ mul.comp (mulLeft (x + y)) = mul.comp (mulLeft x) + mul.comp (mulLeft y)

Tactic:
ext; simp [add_mul]

Goal state after:
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : R
⊢ mul.compr₂ (mulLeft (x + y)) = mul.compr₂ (mulLeft x) + mul.compr₂ (mulLeft y)

Tactic:
ext; simp [add_mul]

Goal state after: