[GOAL]
I : Type u
R : Type u_1
f✝ : I → Type v
x y : (i : I) → f✝ i
i : I
r : CommSemiring R
s : (i : I) → Semiring (f✝ i)
inst✝ : (i : I) → Algebra R (f✝ i)
src✝ : R →+* (i : I) → f✝ i := Pi.ringHom fun i => algebraMap R (f✝ i)
a : R
f : (fun x => (i : I) → f✝ i) a
⊢ ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        a *
      f =
    f *
      ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        a
[PROOFSTEP]
ext
[GOAL]
case h
I : Type u
R : Type u_1
f✝ : I → Type v
x y : (i : I) → f✝ i
i : I
r : CommSemiring R
s : (i : I) → Semiring (f✝ i)
inst✝ : (i : I) → Algebra R (f✝ i)
src✝ : R →+* (i : I) → f✝ i := Pi.ringHom fun i => algebraMap R (f✝ i)
a : R
f : (fun x => (i : I) → f✝ i) a
x✝ : I
⊢ (↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          a *
        f)
      x✝ =
    (f *
        ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          a)
      x✝
[PROOFSTEP]
simp [Algebra.commutes]
[GOAL]
I : Type u
R : Type u_1
f✝ : I → Type v
x y : (i : I) → f✝ i
i : I
r : CommSemiring R
s : (i : I) → Semiring (f✝ i)
inst✝ : (i : I) → Algebra R (f✝ i)
src✝ : R →+* (i : I) → f✝ i := Pi.ringHom fun i => algebraMap R (f✝ i)
a : R
f : (fun x => (i : I) → f✝ i) a
⊢ a • f =
    ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        a *
      f
[PROOFSTEP]
ext
[GOAL]
case h
I : Type u
R : Type u_1
f✝ : I → Type v
x y : (i : I) → f✝ i
i : I
r : CommSemiring R
s : (i : I) → Semiring (f✝ i)
inst✝ : (i : I) → Algebra R (f✝ i)
src✝ : R →+* (i : I) → f✝ i := Pi.ringHom fun i => algebraMap R (f✝ i)
a : R
f : (fun x => (i : I) → f✝ i) a
x✝ : I
⊢ (a • f) x✝ =
    (↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
          a *
        f)
      x✝
[PROOFSTEP]
simp [Algebra.smul_def]
[GOAL]
R : Type u
A : Type v
B : Type w
I✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Type u_2
src✝ : (I → A) →+* I → B := RingHom.compLeft (↑f) I
c : R
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun h => ↑f ∘ h, map_one' := (_ : OneHom.toFun (↑↑src✝) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : I → A),
                      OneHom.toFun (↑↑src✝) (x * y) = OneHom.toFun (↑↑src✝) x * OneHom.toFun (↑↑src✝) y) },
            map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : I → A), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R (I → A)) c) =
    ↑(algebraMap R (I → B)) c
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
A : Type v
B : Type w
I✝ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Type u_2
src✝ : (I → A) →+* I → B := RingHom.compLeft (↑f) I
c : R
x✝ : I
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun h => ↑f ∘ h, map_one' := (_ : OneHom.toFun (↑↑src✝) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : I → A),
                      OneHom.toFun (↑↑src✝) (x * y) = OneHom.toFun (↑↑src✝) x * OneHom.toFun (↑↑src✝) y) },
            map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : I → A), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R (I → A)) c) x✝ =
    ↑(algebraMap R (I → B)) c x✝
[PROOFSTEP]
exact f.commutes' c
[GOAL]
R : Type u_1
ι : Type u_2
A₁ : ι → Type u_3
A₂ : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Semiring (A₁ i)
inst✝² : (i : ι) → Semiring (A₂ i)
inst✝¹ : (i : ι) → Algebra R (A₁ i)
inst✝ : (i : ι) → Algebra R (A₂ i)
e : (i : ι) → A₁ i ≃ₐ[R] A₂ i
src✝ : ((i : ι) → A₁ i) ≃+* ((i : ι) → A₂ i) := RingEquiv.piCongrRight fun i => toRingEquiv (e i)
r : R
⊢ Equiv.toFun
      { toFun := fun x j => ↑(e j) (x j), invFun := fun x j => ↑(symm (e j)) (x j),
        left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (↑(algebraMap R ((i : ι) → A₁ i)) r) =
    ↑(algebraMap R ((i : ι) → A₂ i)) r
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u_1
ι : Type u_2
A₁ : ι → Type u_3
A₂ : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Semiring (A₁ i)
inst✝² : (i : ι) → Semiring (A₂ i)
inst✝¹ : (i : ι) → Algebra R (A₁ i)
inst✝ : (i : ι) → Algebra R (A₂ i)
e : (i : ι) → A₁ i ≃ₐ[R] A₂ i
src✝ : ((i : ι) → A₁ i) ≃+* ((i : ι) → A₂ i) := RingEquiv.piCongrRight fun i => toRingEquiv (e i)
r : R
i : ι
⊢ Equiv.toFun
      { toFun := fun x j => ↑(e j) (x j), invFun := fun x j => ↑(symm (e j)) (x j),
        left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (↑(algebraMap R ((i : ι) → A₁ i)) r) i =
    ↑(algebraMap R ((i : ι) → A₂ i)) r i
[PROOFSTEP]
simp


[GOAL]
R✝ : Type u_1
S : Type u_2
A✝ : Type u_3
B : Type u_4
inst✝¹² : CommSemiring R✝
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A✝
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R✝ S
inst✝⁷ : Algebra R✝ A✝
inst✝⁶ : Algebra R✝ B
inst✝⁵ : Algebra S A✝
inst✝⁴ : SMulCommClass R✝ S A✝
inst✝³ : IsScalarTower R✝ S A✝
R : Type ?u.2035
A : Type ?u.2038
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
x : A
⊢ ↑(RingHom.toOpposite (algebraMap R A)
            (_ :
              ∀ (x y : R),
                ↑(algebraMap R ((fun x => A) x)) x * ↑(algebraMap R A) y =
                  ↑(algebraMap R A) y * ↑(algebraMap R ((fun x => A) x)) x))
        r *
      op x =
    op x *
      ↑(RingHom.toOpposite (algebraMap R A)
            (_ :
              ∀ (x y : R),
                ↑(algebraMap R ((fun x => A) x)) x * ↑(algebraMap R A) y =
                  ↑(algebraMap R A) y * ↑(algebraMap R ((fun x => A) x)) x))
        r
[PROOFSTEP]
simp only [RingHom.toOpposite_apply, Function.comp_apply, ← op_mul, Algebra.commutes]
[GOAL]
R✝ : Type u_1
S : Type u_2
A✝ : Type u_3
B : Type u_4
inst✝¹² : CommSemiring R✝
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A✝
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R✝ S
inst✝⁷ : Algebra R✝ A✝
inst✝⁶ : Algebra R✝ B
inst✝⁵ : Algebra S A✝
inst✝⁴ : SMulCommClass R✝ S A✝
inst✝³ : IsScalarTower R✝ S A✝
R : Type ?u.2035
A : Type ?u.2038
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
c : R
x : (fun x => Aᵐᵒᵖ) c
⊢ unop (c • x) =
    unop
      (↑(RingHom.toOpposite (algebraMap R A)
              (_ :
                ∀ (x y : R),
                  ↑(algebraMap R ((fun x => A) x)) x * ↑(algebraMap R A) y =
                    ↑(algebraMap R A) y * ↑(algebraMap R ((fun x => A) x)) x))
          c *
        x)
[PROOFSTEP]
simp only [unop_smul, RingHom.toOpposite_apply, Function.comp_apply, unop_mul, op_mul, Algebra.smul_def,
  Algebra.commutes, op_unop, unop_op]


[GOAL]
R : Type u
inst✝¹ : CommRing R
D : Type v
inst✝ : SmallCategory D
I : D ⥤ Ideal R
X✝ Y✝ Z✝ : D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun t => ModuleCat.of R (R ⧸ I.obj t),
          map := fun {X Y} w => Submodule.mapQ (I.obj X) (I.obj Y) LinearMap.id (_ : I.obj X ≤ I.obj Y) }.map
      (f ≫ g) =
    { obj := fun t => ModuleCat.of R (R ⧸ I.obj t),
            map := fun {X Y} w => Submodule.mapQ (I.obj X) (I.obj Y) LinearMap.id (_ : I.obj X ≤ I.obj Y) }.map
        f ≫
      { obj := fun t => ModuleCat.of R (R ⧸ I.obj t),
            map := fun {X Y} w => Submodule.mapQ (I.obj X) (I.obj Y) LinearMap.id (_ : I.obj X ≤ I.obj Y) }.map
        g
[PROOFSTEP]
apply Submodule.linearMap_qext
[GOAL]
case h
R : Type u
inst✝¹ : CommRing R
D : Type v
inst✝ : SmallCategory D
I : D ⥤ Ideal R
X✝ Y✝ Z✝ : D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ LinearMap.comp
      ({ obj := fun t => ModuleCat.of R (R ⧸ I.obj t),
            map := fun {X Y} w => Submodule.mapQ (I.obj X) (I.obj Y) LinearMap.id (_ : I.obj X ≤ I.obj Y) }.map
        (f ≫ g))
      (Submodule.mkQ (I.obj X✝)) =
    LinearMap.comp
      ({ obj := fun t => ModuleCat.of R (R ⧸ I.obj t),
              map := fun {X Y} w => Submodule.mapQ (I.obj X) (I.obj Y) LinearMap.id (_ : I.obj X ≤ I.obj Y) }.map
          f ≫
        { obj := fun t => ModuleCat.of R (R ⧸ I.obj t),
              map := fun {X Y} w => Submodule.mapQ (I.obj X) (I.obj Y) LinearMap.id (_ : I.obj X ≤ I.obj Y) }.map
          g)
      (Submodule.mkQ (I.obj X✝))
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
J : Ideal R
k : ℕᵒᵖ
⊢ J ≤ Ideal.radical ((idealPowersDiagram J).obj k)
[PROOFSTEP]
change _ ≤ (J ^ unop k).radical
[GOAL]
R : Type u
inst✝ : CommRing R
J : Ideal R
k : ℕᵒᵖ
⊢ J ≤ Ideal.radical (J ^ k.unop)
[PROOFSTEP]
cases' unop k with n
[GOAL]
case zero
R : Type u
inst✝ : CommRing R
J : Ideal R
k : ℕᵒᵖ
⊢ J ≤ Ideal.radical (J ^ Nat.zero)
[PROOFSTEP]
simp [Ideal.radical_top, pow_zero, Ideal.one_eq_top, le_top, Nat.zero_eq]
[GOAL]
case succ
R : Type u
inst✝ : CommRing R
J : Ideal R
k : ℕᵒᵖ
n : ℕ
⊢ J ≤ Ideal.radical (J ^ Nat.succ n)
[PROOFSTEP]
simp only [J.radical_pow _ n.succ_pos, Ideal.le_radical]
[GOAL]
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hIJ : I ≤ Ideal.radical J
hJ : Ideal.FG (Ideal.radical J)
⊢ ∃ k, I ^ k ≤ J
[PROOFSTEP]
obtain ⟨k, hk⟩ := J.exists_radical_pow_le_of_fg hJ
[GOAL]
case intro
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hIJ : I ≤ Ideal.radical J
hJ : Ideal.FG (Ideal.radical J)
k : ℕ
hk : Ideal.radical J ^ k ≤ J
⊢ ∃ k, I ^ k ≤ J
[PROOFSTEP]
use k
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hIJ : I ≤ Ideal.radical J
hJ : Ideal.FG (Ideal.radical J)
k : ℕ
hk : Ideal.radical J ^ k ≤ J
⊢ I ^ k ≤ J
[PROOFSTEP]
calc
  I ^ k ≤ J.radical ^ k := Ideal.pow_mono hIJ _
  _ ≤ J := hk
[GOAL]
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ IsConnected (CostructuredArrow (idealPowersToSelfLERadical J) J')
[PROOFSTEP]
apply (config := { allowSynthFailures := true }) zigzag_isConnected
[GOAL]
case inst
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ Nonempty (CostructuredArrow (idealPowersToSelfLERadical J) J')
[PROOFSTEP]
obtain ⟨k, hk⟩ := Ideal.exists_pow_le_of_le_radical_of_fG J'.2 (isNoetherian_def.mp hR _)
[GOAL]
case inst.intro
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
k : ℕ
hk : J ^ k ≤ J'.obj
⊢ Nonempty (CostructuredArrow (idealPowersToSelfLERadical J) J')
[PROOFSTEP]
exact ⟨CostructuredArrow.mk (⟨⟨hk⟩⟩ : (idealPowersToSelfLERadical J).obj (op k) ⟶ J')⟩
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ ∀ (j₁ j₂ : CostructuredArrow (idealPowersToSelfLERadical J) J'), Zigzag j₁ j₂
[PROOFSTEP]
intro j1 j2
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
⊢ Zigzag j1 j2
[PROOFSTEP]
apply Relation.ReflTransGen.single
[GOAL]
case h.hab
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
⊢ Zag j1 j2
[PROOFSTEP]
cases' le_total (unop j1.left) (unop j2.left) with h h
[GOAL]
case h.hab.inl
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : j1.left.unop ≤ j2.left.unop
⊢ Zag j1 j2
case h.hab.inr
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : j2.left.unop ≤ j1.left.unop
⊢ Zag j1 j2
[PROOFSTEP]
right
[GOAL]
case h.hab.inl.h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : j1.left.unop ≤ j2.left.unop
⊢ Nonempty (j2 ⟶ j1)
case h.hab.inr
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : j2.left.unop ≤ j1.left.unop
⊢ Zag j1 j2
[PROOFSTEP]
exact ⟨CostructuredArrow.homMk (homOfLE h).op (AsTrue.get trivial)⟩
[GOAL]
case h.hab.inr
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : j2.left.unop ≤ j1.left.unop
⊢ Zag j1 j2
[PROOFSTEP]
left
[GOAL]
case h.hab.inr.h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : j2.left.unop ≤ j1.left.unop
⊢ Nonempty (j1 ⟶ j2)
[PROOFSTEP]
exact ⟨CostructuredArrow.homMk (homOfLE h).op (AsTrue.get trivial)⟩
[GOAL]
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hJK : Ideal.radical J = Ideal.radical K
L : Ideal R
hL : J ≤ Ideal.radical L
⊢ K ≤ Ideal.radical L
[PROOFSTEP]
rw [← Ideal.radical_le_radical_iff] at hL ⊢
[GOAL]
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hJK : Ideal.radical J = Ideal.radical K
L : Ideal R
hL : Ideal.radical J ≤ Ideal.radical L
⊢ Ideal.radical K ≤ Ideal.radical L
[PROOFSTEP]
exact hJK.symm.trans_le hL


[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.24757, u_1} J
inst✝¹ : Category.{?u.24761, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
⊢ whiskerLeft F π₁Toπ₂ ≫ whiskerLeft F π₂Toπ₃ = 0
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.24757, u_1} J
inst✝¹ : Category.{?u.24761, u_2} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : J ⥤ ShortComplex C
φ : X✝ ⟶ Y✝
⊢ whiskerRight φ π₁ ≫
      ((fun F => mk (whiskerLeft F π₁Toπ₂) (whiskerLeft F π₂Toπ₃) (_ : whiskerLeft F π₁Toπ₂ ≫ whiskerLeft F π₂Toπ₃ = 0))
          Y✝).f =
    ((fun F => mk (whiskerLeft F π₁Toπ₂) (whiskerLeft F π₂Toπ₃) (_ : whiskerLeft F π₁Toπ₂ ≫ whiskerLeft F π₂Toπ₃ = 0))
          X✝).f ≫
      whiskerRight φ π₂
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.24757, u_1} J
inst✝¹ : Category.{?u.24761, u_2} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : J ⥤ ShortComplex C
φ : X✝ ⟶ Y✝
⊢ whiskerRight φ π₂ ≫
      ((fun F => mk (whiskerLeft F π₁Toπ₂) (whiskerLeft F π₂Toπ₃) (_ : whiskerLeft F π₁Toπ₂ ≫ whiskerLeft F π₂Toπ₃ = 0))
          Y✝).g =
    ((fun F => mk (whiskerLeft F π₁Toπ₂) (whiskerLeft F π₂Toπ₃) (_ : whiskerLeft F π₁Toπ₂ ≫ whiskerLeft F π₂Toπ₃ = 0))
          X✝).g ≫
      whiskerRight φ π₃
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.53514, u_1} J
inst✝¹ : Category.{?u.53518, u_2} C
inst✝ : HasZeroMorphisms C
x✝ : ShortComplex (J ⥤ C)
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    ((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₁.map f ≫
        ((fun x => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₁.obj x)) Y).hom =
      ((fun x => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₁.obj x)) X).hom ≫
        ((functor J C ⋙ inverse J C).obj x✝).X₁.map f
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.53514, u_1} J
inst✝¹ : Category.{?u.53518, u_2} C
inst✝ : HasZeroMorphisms C
x✝ : ShortComplex (J ⥤ C)
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    ((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₂.map f ≫
        ((fun x => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₂.obj x)) Y).hom =
      ((fun x => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₂.obj x)) X).hom ≫
        ((functor J C ⋙ inverse J C).obj x✝).X₂.map f
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.53514, u_1} J
inst✝¹ : Category.{?u.53518, u_2} C
inst✝ : HasZeroMorphisms C
x✝ : ShortComplex (J ⥤ C)
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    ((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₃.map f ≫
        ((fun x => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₃.obj x)) Y).hom =
      ((fun x => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₃.obj x)) X).hom ≫
        ((functor J C ⋙ inverse J C).obj x✝).X₃.map f
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.53514, u_1} J
inst✝¹ : Category.{?u.53518, u_2} C
inst✝ : HasZeroMorphisms C
x✝ : ShortComplex (J ⥤ C)
⊢ (NatIso.ofComponents fun x => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₁.obj x)).hom ≫
      ((functor J C ⋙ inverse J C).obj x✝).f =
    ((𝟭 (ShortComplex (J ⥤ C))).obj x✝).f ≫
      (NatIso.ofComponents fun x => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₂.obj x)).hom
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.53514, u_1} J
inst✝¹ : Category.{?u.53518, u_2} C
inst✝ : HasZeroMorphisms C
x✝ : ShortComplex (J ⥤ C)
⊢ (NatIso.ofComponents fun x => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₂.obj x)).hom ≫
      ((functor J C ⋙ inverse J C).obj x✝).g =
    ((𝟭 (ShortComplex (J ⥤ C))).obj x✝).g ≫
      (NatIso.ofComponents fun x => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₃.obj x)).hom
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.53514, u_1} J
inst✝¹ : Category.{?u.53518, u_2} C
inst✝ : HasZeroMorphisms C
⊢ ∀ {X Y : ShortComplex (J ⥤ C)} (f : X ⟶ Y),
    (𝟭 (ShortComplex (J ⥤ C))).map f ≫
        ((fun x =>
              isoMk (NatIso.ofComponents fun x_1 => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x).X₁.obj x_1))
                (NatIso.ofComponents fun x_1 => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x).X₂.obj x_1))
                (NatIso.ofComponents fun x_1 => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x).X₃.obj x_1)))
            Y).hom =
      ((fun x =>
              isoMk (NatIso.ofComponents fun x_1 => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x).X₁.obj x_1))
                (NatIso.ofComponents fun x_1 => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x).X₂.obj x_1))
                (NatIso.ofComponents fun x_1 => Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x).X₃.obj x_1)))
            X).hom ≫
        (functor J C ⋙ inverse J C).map f
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.111338, u_1} J
inst✝¹ : Category.{?u.111342, u_2} C
inst✝ : HasZeroMorphisms C
x✝¹ : J ⥤ ShortComplex C
x✝ : J
⊢ (Iso.refl (((inverse J C ⋙ functor J C).obj x✝¹).obj x✝).X₁).hom ≫ (((𝟭 (J ⥤ ShortComplex C)).obj x✝¹).obj x✝).f =
    (((inverse J C ⋙ functor J C).obj x✝¹).obj x✝).f ≫ (Iso.refl (((inverse J C ⋙ functor J C).obj x✝¹).obj x✝).X₂).hom
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.111338, u_1} J
inst✝¹ : Category.{?u.111342, u_2} C
inst✝ : HasZeroMorphisms C
x✝¹ : J ⥤ ShortComplex C
x✝ : J
⊢ (Iso.refl (((inverse J C ⋙ functor J C).obj x✝¹).obj x✝).X₂).hom ≫ (((𝟭 (J ⥤ ShortComplex C)).obj x✝¹).obj x✝).g =
    (((inverse J C ⋙ functor J C).obj x✝¹).obj x✝).g ≫ (Iso.refl (((inverse J C ⋙ functor J C).obj x✝¹).obj x✝).X₃).hom
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.111338, u_1} J
inst✝¹ : Category.{?u.111342, u_2} C
inst✝ : HasZeroMorphisms C
x✝ : J ⥤ ShortComplex C
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    ((inverse J C ⋙ functor J C).obj x✝).map f ≫
        ((fun x =>
              isoMk (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj x).X₁)
                (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj x).X₂)
                (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj x).X₃))
            Y).hom =
      ((fun x =>
              isoMk (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj x).X₁)
                (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj x).X₂)
                (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj x).X₃))
            X).hom ≫
        ((𝟭 (J ⥤ ShortComplex C)).obj x✝).map f
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u_1
C : Type u_2
inst✝² : Category.{?u.111338, u_1} J
inst✝¹ : Category.{?u.111342, u_2} C
inst✝ : HasZeroMorphisms C
⊢ ∀ {X Y : J ⥤ ShortComplex C} (f : X ⟶ Y),
    (inverse J C ⋙ functor J C).map f ≫
        ((fun x =>
              NatIso.ofComponents fun x_1 =>
                isoMk (Iso.refl (((inverse J C ⋙ functor J C).obj x).obj x_1).X₁)
                  (Iso.refl (((inverse J C ⋙ functor J C).obj x).obj x_1).X₂)
                  (Iso.refl (((inverse J C ⋙ functor J C).obj x).obj x_1).X₃))
            Y).hom =
      ((fun x =>
              NatIso.ofComponents fun x_1 =>
                isoMk (Iso.refl (((inverse J C ⋙ functor J C).obj x).obj x_1).X₁)
                  (Iso.refl (((inverse J C ⋙ functor J C).obj x).obj x_1).X₂)
                  (Iso.refl (((inverse J C ⋙ functor J C).obj x).obj x_1).X₃))
            X).hom ≫
        (𝟭 (J ⥤ ShortComplex C)).map f
[PROOFSTEP]
aesop_cat