[GOAL]
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
A : Rep k G
f g : (Fin n → G) → CoeSort.coe A
⊢ (fun f g =>
        ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
          Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
      (f + g) =
    (fun f g =>
          ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
            Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
        f +
      (fun f g =>
          ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
            Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
        g
[PROOFSTEP]
ext x
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
A : Rep k G
f g : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ (fun f g =>
        ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
          Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
      (f + g) x =
    ((fun f g =>
            ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
              Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
          f +
        (fun f g =>
            ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
              Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
          g)
      x
[PROOFSTEP]
simp_rw [Pi.add_apply, map_add, smul_add, Finset.sum_add_distrib, add_add_add_comm]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
A : Rep k G
r : k
f : (Fin n → G) → CoeSort.coe A
⊢ AddHom.toFun
      {
        toFun := fun f g =>
          ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
            Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g),
        map_add' :=
          (_ :
            ∀ (f g : (Fin n → G) → CoeSort.coe A),
              (fun f g =>
                    ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                      Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                  (f + g) =
                (fun f g =>
                      ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                        Finset.sum Finset.univ fun j =>
                          (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                    f +
                  (fun f g =>
                      ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                        Finset.sum Finset.univ fun j =>
                          (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                    g) }
      (r • f) =
    ↑(RingHom.id k) r •
      AddHom.toFun
        {
          toFun := fun f g =>
            ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
              Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g),
          map_add' :=
            (_ :
              ∀ (f g : (Fin n → G) → CoeSort.coe A),
                (fun f g =>
                      ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                        Finset.sum Finset.univ fun j =>
                          (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                    (f + g) =
                  (fun f g =>
                        ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                          Finset.sum Finset.univ fun j =>
                            (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                      f +
                    (fun f g =>
                        ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                          Finset.sum Finset.univ fun j =>
                            (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                      g) }
        f
[PROOFSTEP]
ext x
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
A : Rep k G
r : k
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ AddHom.toFun
      {
        toFun := fun f g =>
          ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
            Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g),
        map_add' :=
          (_ :
            ∀ (f g : (Fin n → G) → CoeSort.coe A),
              (fun f g =>
                    ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                      Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                  (f + g) =
                (fun f g =>
                      ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                        Finset.sum Finset.univ fun j =>
                          (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                    f +
                  (fun f g =>
                      ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                        Finset.sum Finset.univ fun j =>
                          (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                    g) }
      (r • f) x =
    (↑(RingHom.id k) r •
        AddHom.toFun
          {
            toFun := fun f g =>
              ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g),
            map_add' :=
              (_ :
                ∀ (f g : (Fin n → G) → CoeSort.coe A),
                  (fun f g =>
                        ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                          Finset.sum Finset.univ fun j =>
                            (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                      (f + g) =
                    (fun f g =>
                          ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                            Finset.sum Finset.univ fun j =>
                              (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                        f +
                      (fun f g =>
                          ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                            Finset.sum Finset.univ fun j =>
                              (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                        g) }
          f)
      x
[PROOFSTEP]
simp_rw [Pi.smul_apply, RingHom.id_apply, map_smul, smul_add, Finset.smul_sum, ← smul_assoc, smul_eq_mul, mul_comm r]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
⊢ d n A =
    (LinearEquiv.toModuleIso (diagonalHomEquiv n A)).inv ≫
      HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1) ≫
        (LinearEquiv.toModuleIso (diagonalHomEquiv (n + 1) A)).hom
[PROOFSTEP]
ext f g
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ ↑(d n A) f g =
    ↑((LinearEquiv.toModuleIso (diagonalHomEquiv n A)).inv ≫
          HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1) ≫
            (LinearEquiv.toModuleIso (diagonalHomEquiv (n + 1) A)).hom)
      f g
[PROOFSTEP]
change d n A f g = diagonalHomEquiv (n + 1) A ((resolution k G).d (n + 1) n ≫ (diagonalHomEquiv n A).symm f) g
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ ↑(d n A) f g =
    ↑(diagonalHomEquiv (n + 1) A)
      (HomologicalComplex.d (resolution k G) (n + 1) n ≫ ↑(LinearEquiv.symm (diagonalHomEquiv n A)) f) g
[PROOFSTEP]
rw [diagonalHomEquiv_apply, Action.comp_hom, ModuleCat.comp_def, LinearMap.comp_apply, Resolution.d_eq]
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ ↑(d n A) f g =
    ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom
      (↑(Resolution.d k G (n + 1)) (Finsupp.single (Fin.partialProd g) 1))
[PROOFSTEP]
erw [Resolution.d_of (Fin.partialProd g)]
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ ↑(d n A) f g =
    ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom
      (Finset.sum Finset.univ fun p => Finsupp.single (Fin.partialProd g ∘ Fin.succAbove p) ((-1) ^ ↑p))
[PROOFSTEP]
rw [LinearMap.map_sum]
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ ↑(d n A) f g =
    Finset.sum Finset.univ fun i =>
      ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom
        (Finsupp.single (Fin.partialProd g ∘ Fin.succAbove i) ((-1) ^ ↑i))
[PROOFSTEP]
simp only [← Finsupp.smul_single_one _ ((-1 : k) ^ _)]
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ ↑(d n A) f g =
    Finset.sum Finset.univ fun x =>
      ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom
        ((-1) ^ ↑x • Finsupp.single (Fin.partialProd g ∘ Fin.succAbove x) 1)
[PROOFSTEP]
rw [d_apply, @Fin.sum_univ_succ _ _ (n + 1), Fin.val_zero, pow_zero, one_smul, Fin.succAbove_zero,
  diagonalHomEquiv_symm_apply f (Fin.partialProd g ∘ @Fin.succ (n + 1))]
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ (↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
      Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g)) =
    ↑(↑(ρ A) ((Fin.partialProd g ∘ Fin.succ) 0))
        (f fun i => ((Fin.partialProd g ∘ Fin.succ) (Fin.castSucc i))⁻¹ * (Fin.partialProd g ∘ Fin.succ) (Fin.succ i)) +
      Finset.sum Finset.univ fun i =>
        ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom
          ((-1) ^ ↑(Fin.succ i) • Finsupp.single (Fin.partialProd g ∘ Fin.succAbove (Fin.succ i)) 1)
[PROOFSTEP]
simp_rw [Function.comp_apply, Fin.partialProd_succ, Fin.castSucc_zero, Fin.partialProd_zero, one_mul]
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ (↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
      Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g)) =
    ↑(↑(ρ A) (g 0))
        (f fun i =>
          (Fin.partialProd g (Fin.castSucc (Fin.castSucc i)) * g (Fin.castSucc i))⁻¹ *
            (Fin.partialProd g (Fin.castSucc (Fin.succ i)) * g (Fin.succ i))) +
      Finset.sum Finset.univ fun i =>
        ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom
          ((-1) ^ ↑(Fin.succ i) • Finsupp.single (Fin.partialProd g ∘ Fin.succAbove (Fin.succ i)) 1)
[PROOFSTEP]
rcongr x
[GOAL]
case h.h.e_a.h.e_6.h.e_a.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
x : Fin n
⊢ g (Fin.succ x) =
    (Fin.partialProd g (Fin.castSucc (Fin.castSucc x)) * g (Fin.castSucc x))⁻¹ *
      (Fin.partialProd g (Fin.castSucc (Fin.succ x)) * g (Fin.succ x))
[PROOFSTEP]
have := Fin.partialProd_right_inv g (Fin.castSucc x)
[GOAL]
case h.h.e_a.h.e_6.h.e_a.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
x : Fin n
this :
  (Fin.partialProd g (Fin.castSucc (Fin.castSucc x)))⁻¹ * Fin.partialProd g (Fin.succ (Fin.castSucc x)) =
    g (Fin.castSucc x)
⊢ g (Fin.succ x) =
    (Fin.partialProd g (Fin.castSucc (Fin.castSucc x)) * g (Fin.castSucc x))⁻¹ *
      (Fin.partialProd g (Fin.castSucc (Fin.succ x)) * g (Fin.succ x))
[PROOFSTEP]
simp only [mul_inv_rev, Fin.castSucc_fin_succ] at this ⊢
[GOAL]
case h.h.e_a.h.e_6.h.e_a.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
x : Fin n
this :
  (Fin.partialProd g (Fin.castSucc (Fin.castSucc x)))⁻¹ * Fin.partialProd g (Fin.succ (Fin.castSucc x)) =
    g (Fin.castSucc x)
⊢ g (Fin.succ x) =
    (g (Fin.castSucc x))⁻¹ * (Fin.partialProd g (Fin.castSucc (Fin.castSucc x)))⁻¹ *
      (Fin.partialProd g (Fin.succ (Fin.castSucc x)) * g (Fin.succ x))
[PROOFSTEP]
rw [mul_assoc, ← mul_assoc _ _ (g x.succ), this, inv_mul_cancel_left]
[GOAL]
case h.h.e_a.e_f.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
x : Fin (n + 1)
⊢ (-1) ^ (↑x + 1) • f (Fin.contractNth x (fun x x_1 => x * x_1) g) =
    ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom
      ((-1) ^ ↑(Fin.succ x) • Finsupp.single (Fin.partialProd g ∘ Fin.succAbove (Fin.succ x)) 1)
[PROOFSTEP]
rw [map_smul, diagonalHomEquiv_symm_partialProd_succ, Fin.val_succ]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ (fun n => d n A) n ≫ (fun n => d n A) (n + 1) = 0
[PROOFSTEP]
ext x
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
x : ↑((fun n => ModuleCat.of k ((Fin n → G) → CoeSort.coe A)) n)
⊢ ↑((fun n => d n A) n ≫ (fun n => d n A) (n + 1)) x = ↑0 x
[PROOFSTEP]
have := LinearMap.ext_iff.1 ((linearYonedaObjResolution A).d_comp_d n (n + 1) (n + 2))
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
x : ↑((fun n => ModuleCat.of k ((Fin n → G) → CoeSort.coe A)) n)
this :
  ∀ (x : ↑(HomologicalComplex.X (linearYonedaObjResolution A) n)),
    ↑(HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1) ≫
            HomologicalComplex.d (linearYonedaObjResolution A) (n + 1) (n + 2))
        x =
      ↑0 x
⊢ ↑((fun n => d n A) n ≫ (fun n => d n A) (n + 1)) x = ↑0 x
[PROOFSTEP]
simp only [ModuleCat.comp_def, LinearMap.comp_apply] at this 
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
x : ↑((fun n => ModuleCat.of k ((Fin n → G) → CoeSort.coe A)) n)
this :
  ∀ (x : ↑(HomologicalComplex.X (linearYonedaObjResolution A) n)),
    ↑(HomologicalComplex.d (linearYonedaObjResolution A) (n + 1) (n + 2))
        (↑(HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1)) x) =
      ↑0 x
⊢ ↑((fun n => d n A) n ≫ (fun n => d n A) (n + 1)) x = ↑0 x
[PROOFSTEP]
dsimp only
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
x : ↑((fun n => ModuleCat.of k ((Fin n → G) → CoeSort.coe A)) n)
this :
  ∀ (x : ↑(HomologicalComplex.X (linearYonedaObjResolution A) n)),
    ↑(HomologicalComplex.d (linearYonedaObjResolution A) (n + 1) (n + 2))
        (↑(HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1)) x) =
      ↑0 x
⊢ ↑(d n A ≫ d (n + 1) A) x = ↑0 x
[PROOFSTEP]
simp only [d_eq, LinearEquiv.toModuleIso_inv, LinearEquiv.toModuleIso_hom, ModuleCat.coe_comp, Function.comp_apply]
  /- Porting note: I can see I need to rewrite `LinearEquiv.coe_coe` twice to at
        least reduce the need for `symm_apply_apply` to be an `erw`. However, even `erw` refuses to
        rewrite the second `coe_coe`... -/
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
x : ↑((fun n => ModuleCat.of k ((Fin n → G) → CoeSort.coe A)) n)
this :
  ∀ (x : ↑(HomologicalComplex.X (linearYonedaObjResolution A) n)),
    ↑(HomologicalComplex.d (linearYonedaObjResolution A) (n + 1) (n + 2))
        (↑(HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1)) x) =
      ↑0 x
⊢ ↑↑(Rep.diagonalHomEquiv (n + 1 + 1) A)
      (↑(HomologicalComplex.d (linearYonedaObjResolution A) (n + 1) (n + 1 + 1))
        (↑↑(LinearEquiv.symm (Rep.diagonalHomEquiv (n + 1) A))
          (↑↑(Rep.diagonalHomEquiv (n + 1) A)
            (↑(HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1))
              (↑↑(LinearEquiv.symm (Rep.diagonalHomEquiv n A)) x))))) =
    ↑0 x
[PROOFSTEP]
erw [LinearEquiv.symm_apply_apply, this]
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
x : ↑((fun n => ModuleCat.of k ((Fin n → G) → CoeSort.coe A)) n)
this :
  ∀ (x : ↑(HomologicalComplex.X (linearYonedaObjResolution A) n)),
    ↑(HomologicalComplex.d (linearYonedaObjResolution A) (n + 1) (n + 2))
        (↑(HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1)) x) =
      ↑0 x
⊢ ↑↑(Rep.diagonalHomEquiv (n + 1 + 1) A) (↑0 (↑↑(LinearEquiv.symm (Rep.diagonalHomEquiv n A)) x)) = ↑0 x
[PROOFSTEP]
exact map_zero _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
⊢ inhomogeneousCochains A ≅ linearYonedaObjResolution A
[PROOFSTEP]
refine' HomologicalComplex.Hom.isoOfComponents (fun i => (Rep.diagonalHomEquiv i A).toModuleIso.symm) _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
⊢ ∀ (i j : ℕ),
    ComplexShape.Rel (ComplexShape.up ℕ) i j →
      ((fun i => (LinearEquiv.toModuleIso (Rep.diagonalHomEquiv i A)).symm) i).hom ≫
          HomologicalComplex.d (linearYonedaObjResolution A) i j =
        HomologicalComplex.d (inhomogeneousCochains A) i j ≫
          ((fun i => (LinearEquiv.toModuleIso (Rep.diagonalHomEquiv i A)).symm) j).hom
[PROOFSTEP]
rintro i j (h : i + 1 = j)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
i j : ℕ
h : i + 1 = j
⊢ ((fun i => (LinearEquiv.toModuleIso (Rep.diagonalHomEquiv i A)).symm) i).hom ≫
      HomologicalComplex.d (linearYonedaObjResolution A) i j =
    HomologicalComplex.d (inhomogeneousCochains A) i j ≫
      ((fun i => (LinearEquiv.toModuleIso (Rep.diagonalHomEquiv i A)).symm) j).hom
[PROOFSTEP]
subst h
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
i : ℕ
⊢ ((fun i => (LinearEquiv.toModuleIso (Rep.diagonalHomEquiv i A)).symm) i).hom ≫
      HomologicalComplex.d (linearYonedaObjResolution A) i (i + 1) =
    HomologicalComplex.d (inhomogeneousCochains A) i (i + 1) ≫
      ((fun i => (LinearEquiv.toModuleIso (Rep.diagonalHomEquiv i A)).symm) (i + 1)).hom
[PROOFSTEP]
simp only [CochainComplex.of_d, d_eq, Category.assoc, Iso.symm_hom, Iso.hom_inv_id, Category.comp_id]
