mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : iSupIndep Subtype.val
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ ((DFinsupp.lsum ℕ) fun i ↦ (↑i).subtype).range = ⊤

Tactic:
rw [← Submodule.iSup_eq_range_dfinsupp_lsum, ← sSup, sSup_eq_iSup']

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
i : ℕ
⊢ (a✝ * b✝).coeff i ∈ I ^ i

Tactic:
coeff_mul

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
i : ℕ
⊢ ∑ x ∈ Finset.antidiagonal i, a✝.coeff x.1 * b✝.coeff x.2 ∈ I ^ i
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
r : R[X]
n : ℕ
a : R
⊢ (toFinsuppIso R).symm (AddMonoidAlgebra.coeffAddEquiv.symm (coeffAddEquiv (r • single R n a))) =
    r * (toFinsuppIso R).symm (AddMonoidAlgebra.coeffAddEquiv.symm (coeffAddEquiv (single R n a)))

Tactic:
ext i
    simp only [coeffAddEquiv_apply, AddMonoidAlgebra.coeffAddEquiv_symm_apply,
      toFinsuppIso_symm_apply, coeff_ofFinsupp, smul_single_apply, smul_eq_mul, coeff_single,
      AddMonoidAlgebra.ofCoeff_single, ofFinsupp_single]
    split_ifs with hn
    · rw [show i = (i - n) + n by lia, Polynomial.coeff_mul_monomial]
      simp
    · rw [Polynomial.coeff_mul, Finset.sum_eq_zero]
      simp [Polynomial.coeff_monomial]
      lia

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
a : ℕ
⊢ f.coeff a ∈ I ^ a ↔ a ∈ f.support → f.coeff a ∈ I ^ a

Tactic:
mem_support_iff,

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
a : ℕ
⊢ f.coeff a ∈ I ^ a ↔ f.coeff a ≠ 0 → f.coeff a ∈ I ^ a
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : Infinite R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
h : y ≠ 0
r s : R
hrs : x + r • y = x + s • y
⊢ r = s

Tactic:
rw [add_right_inj] at hrs

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : Infinite R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
h : y ≠ 0
r s : R
hrs : r • y = s • y
⊢ r = s
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ I.cotangentIdeal ^ 2 = ⊥

Tactic:
rw [eq_bot_iff, pow_two I.cotangentIdeal, ← smul_eq_mul]
  intro x hx
  refine Submodule.smul_induction_on hx ?_ ?_
  · rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩; apply (Submodule.Quotient.eq _).mpr _
    rw [sub_zero, pow_two]; exact Ideal.mul_mem_mul hx hy
  · intro x y hx hy; exact add_mem hx hy

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
⊢ Submodule.map (maximalIdeal R).toCotangent M = ⊤ ↔ M = ⊤

Tactic:
refine ⟨fun H ↦ eq_top_iff.mpr ?_, by rintro rfl; simp [Ideal.toCotangent_range]⟩

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
H : Submodule.map (maximalIdeal R).toCotangent M = ⊤
⊢ ⊤ ≤ M
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ X (f b) = X (g b)

Tactic:
simp only [h]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ X (g b) = X (f b)

Tactic:
simp only [h]

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ ((h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫ (h.add (m₁ + m₂) m₃).inv.app X) ≫
      (h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X) =
    ((h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫ (h.add m₁ (m₂ + m₃)).inv.app X ≫ eqToHom ⋯) ≫
      (h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)

Tactic:
Category.assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ (h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫
      (h.add (m₁ + m₂) m₃).inv.app X ≫ (h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X) =
    ((h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫ (h.add m₁ (m₂ + m₃)).inv.app X ≫ eqToHom ⋯) ≫
      (h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ (h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫
      (h.add (m₁ + m₂) m₃).inv.app X ≫ (h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X) =
    ((h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫ (h.add m₁ (m₂ + m₃)).inv.app X ≫ eqToHom ⋯) ≫
      (h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)

Tactic:
Category.assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ (h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫
      (h.add (m₁ + m₂) m₃).inv.app X ≫ (h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X) =
    (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫
      ((h.add m₁ (m₂ + m₃)).inv.app X ≫ eqToHom ⋯) ≫
        (h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ (h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫
      (h.add (m₁ + m₂) m₃).inv.app X ≫ (h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X) =
    (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫
      ((h.add m₁ (m₂ + m₃)).inv.app X ≫ eqToHom ⋯) ≫
        (h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)

Tactic:
Category.assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ (h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫
      (h.add (m₁ + m₂) m₃).inv.app X ≫ (h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X) =
    (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫
      (h.add m₁ (m₂ + m₃)).inv.app X ≫
        eqToHom ⋯ ≫ (h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ 𝟙 ((h.F (0 + n)).obj X) = (eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X)) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯

Tactic:
Category.assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ 𝟙 ((h.F (n + 0)).obj X) = (eqToHom ⋯ ≫ h.zero.inv.app ((h.F n).obj X)) ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯

Tactic:
Category.assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ 𝟙 ((h.F (n + 0)).obj X) = eqToHom ⋯ ≫ h.zero.inv.app ((h.F n).obj X) ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
Module: Mathlib.Algebra.Homology.Additive

Goal state before:
pp: ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
i j : ι
h : i ≠ j
X : W₁
⊢ ((singleMapHomologicalComplex F c j).hom.app X).f i = 0

Tactic:
by
  simp [singleMapHomologicalComplex, h]

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

Goal state before:
pp: case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    ((shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
        (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C n).map ((shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
              (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C p').obj X)) ≫
      (shiftFunctorAdd' C p' p 0 hp).inv.app X

Tactic:
Category.assoc,

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      ((shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C n).map ((shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
              (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C p').obj X)) ≫
        (shiftFunctorAdd' C p' p 0 hp).inv.app X
Module: Mathlib.Algebra.Homology.Additive

Goal state before:
pp: ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
i j : ι
h : i ≠ j
X : W₁
⊢ ((singleMapHomologicalComplex F c j).inv.app X).f i = 0

Tactic:
by
  simp [singleMapHomologicalComplex, h]

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

Goal state before:
pp: case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      ((shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C n).map ((shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
              (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C p').obj X)) ≫
        (shiftFunctorAdd' C p' p 0 hp).inv.app X

Tactic:
Category.assoc,

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
        ((shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C n).map ((shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
              (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C p').obj X)) ≫
          (shiftFunctorAdd' C p' p 0 hp).inv.app X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
        ((shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C n).map ((shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
              (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C p').obj X)) ≫
          (shiftFunctorAdd' C p' p 0 hp).inv.app X

Tactic:
Category.assoc,

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
          ((shiftFunctor C n).map ((shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
              (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C p').obj X)) ≫
            (shiftFunctorAdd' C p' p 0 hp).inv.app X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
          ((shiftFunctor C n).map ((shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
              (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C p').obj X)) ≫
            (shiftFunctorAdd' C p' p 0 hp).inv.app X

Tactic:
Category.assoc,

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C n).map ((shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
            (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C p').obj X) ≫ (shiftFunctorAdd' C p' p 0 hp).inv.app X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map
          ((((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X) ≫
                (shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
              (shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)) ≫
            (shiftFunctorAdd' C p' m n' ⋯).inv.app X) ≫
        (shiftFunctorAdd' C n' n 0 ⋯).inv.app X

Tactic:
Category.assoc,

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map
          (((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X) ≫
              (shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X) ≫
              (shiftFunctorAdd' C p' m n' ⋯).inv.app X) ≫
        (shiftFunctorAdd' C n' n 0 ⋯).inv.app X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map
          (((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X) ≫
              (shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X) ≫
              (shiftFunctorAdd' C p' m n' ⋯).inv.app X) ≫
        (shiftFunctorAdd' C n' n 0 ⋯).inv.app X

Tactic:
Category.assoc,

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map
          ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X) ≫
            (shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X) ≫
              (shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X) ≫
                (shiftFunctorAdd' C p' m n' ⋯).inv.app X) ≫
        (shiftFunctorAdd' C n' n 0 ⋯).inv.app X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p' ⋙ shiftFunctor C p).obj X) =
    ((shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
        (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctorCompIsoId C n' n hn).hom.app X) ≫
      (shiftFunctorCompIsoId C n' n hn).inv.app X ≫
        (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).inv.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)

Tactic:
Category.assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p' ⋙ shiftFunctor C p).obj X) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      ((shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctorCompIsoId C n' n hn).hom.app X) ≫
        (shiftFunctorCompIsoId C n' n hn).inv.app X ≫
          (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).inv.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
              (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p' ⋙ shiftFunctor C p).obj X) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      ((shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctorCompIsoId C n' n hn).hom.app X) ≫
        (shiftFunctorCompIsoId C n' n hn).inv.app X ≫
          (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).inv.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
              (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)

Tactic:
Category.assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p' ⋙ shiftFunctor C p).obj X) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        ((shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctorCompIsoId C n' n hn).hom.app X) ≫
          (shiftFunctorCompIsoId C n' n hn).inv.app X ≫
            (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).inv.app ((shiftFunctor C n').obj X)) ≫
              (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
                (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p' ⋙ shiftFunctor C p).obj X) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        ((shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctorCompIsoId C n' n hn).hom.app X) ≫
          (shiftFunctorCompIsoId C n' n hn).inv.app X ≫
            (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).inv.app ((shiftFunctor C n').obj X)) ≫
              (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
                (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)

Tactic:
Category.assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p' ⋙ shiftFunctor C p).obj X) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).hom.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctorCompIsoId C n' n hn).hom.app X ≫
            (shiftFunctorCompIsoId C n' n hn).inv.app X ≫
              (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).inv.app ((shiftFunctor C n').obj X)) ≫
                (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
                  (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)