[GOAL]
k G✝ : Type u
inst✝² : CommRing k
n✝ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n : ℕ
f : Fin (n + 1) → G
⊢ Hom.hom (actionDiagonalSucc G n).hom f = (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i))
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
k G✝ : Type u
inst✝² : CommRing k
n✝ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n : ℕ
f✝ : Fin (n + 1) → G
f : Fin (Nat.zero + 1) → G
⊢ Hom.hom (actionDiagonalSucc G Nat.zero).hom f = (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i))
[PROOFSTEP]
exact Prod.ext rfl (funext fun x => Fin.elim0 x)
[GOAL]
case succ
k G✝ : Type u
inst✝² : CommRing k
n✝¹ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n✝ : ℕ
f✝ : Fin (n✝ + 1) → G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    Hom.hom (actionDiagonalSucc G n).hom f = (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i))
f : Fin (Nat.succ n + 1) → G
⊢ Hom.hom (actionDiagonalSucc G (Nat.succ n)).hom f = (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i))
[PROOFSTEP]
refine'
  Prod.ext rfl
    (funext fun x => _)
      /- Porting note: broken proof was
          · dsimp only [actionDiagonalSucc]
            simp only [Iso.trans_hom, comp_hom, types_comp_apply, diagonalSucc_hom_hom,
              leftRegularTensorIso_hom_hom, tensorIso_hom, mkIso_hom_hom, Equiv.toIso_hom,
              Action.tensorHom, Equiv.piFinSuccAboveEquiv_symm_apply, tensor_apply, types_id_apply,
              tensor_rho, MonoidHom.one_apply, End.one_def, hn fun j : Fin (n + 1) => f j.succ,
              Fin.insertNth_zero']
            refine' Fin.cases (Fin.cons_zero _ _) (fun i => _) x
            · simp only [Fin.cons_succ, mul_left_inj, inv_inj, Fin.castSucc_fin_succ] -/
[GOAL]
case succ
k G✝ : Type u
inst✝² : CommRing k
n✝¹ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n✝ : ℕ
f✝ : Fin (n✝ + 1) → G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    Hom.hom (actionDiagonalSucc G n).hom f = (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i))
f : Fin (Nat.succ n + 1) → G
x : Fin (Nat.succ n)
⊢ Prod.snd (Hom.hom (actionDiagonalSucc G (Nat.succ n)).hom f) x =
    Prod.snd (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i)) x
[PROOFSTEP]
dsimp [actionDiagonalSucc]
[GOAL]
case succ
k G✝ : Type u
inst✝² : CommRing k
n✝¹ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n✝ : ℕ
f✝ : Fin (n✝ + 1) → G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    Hom.hom (actionDiagonalSucc G n).hom f = (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i))
f : Fin (Nat.succ n + 1) → G
x : Fin (Nat.succ n)
⊢ ↑(Equiv.piFinSuccAboveEquiv (fun x => G) 0).symm
      (↑(FunctorCategoryEquivalence.inverse.obj
              (FunctorCategoryEquivalence.functor.obj (leftRegular G) ⊗
                FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 })).ρ
        (↑(Equiv.piFinSuccAboveEquiv (fun a => G) 0) f).fst⁻¹
        (Hom.hom (actionDiagonalSucc G n).hom (↑(Equiv.piFinSuccAboveEquiv (fun a => G) 0) f).snd))
      x =
    (f (Fin.castSucc x))⁻¹ * f (Fin.succ x)
[PROOFSTEP]
erw [hn (fun (j : Fin (n + 1)) => f j.succ)]
[GOAL]
case succ
k G✝ : Type u
inst✝² : CommRing k
n✝¹ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n✝ : ℕ
f✝ : Fin (n✝ + 1) → G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    Hom.hom (actionDiagonalSucc G n).hom f = (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i))
f : Fin (Nat.succ n + 1) → G
x : Fin (Nat.succ n)
⊢ ↑(Equiv.piFinSuccAboveEquiv (fun x => G) 0).symm
      (↑(FunctorCategoryEquivalence.inverse.obj
              (FunctorCategoryEquivalence.functor.obj (leftRegular G) ⊗
                FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 })).ρ
        (↑(Equiv.piFinSuccAboveEquiv (fun a => G) 0) f).fst⁻¹
        (f (Fin.succ 0), fun i => (f (Fin.succ (Fin.castSucc i)))⁻¹ * f (Fin.succ (Fin.succ i))))
      x =
    (f (Fin.castSucc x))⁻¹ * f (Fin.succ x)
[PROOFSTEP]
exact Fin.cases rfl (fun i => rfl) x
[GOAL]
k G✝ : Type u
inst✝² : CommRing k
n✝ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n : ℕ
g : G
f : Fin n → G
⊢ Hom.hom (actionDiagonalSucc G n).inv (g, f) = g • partialProd f
[PROOFSTEP]
revert g
[GOAL]
k G✝ : Type u
inst✝² : CommRing k
n✝ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n : ℕ
f : Fin n → G
⊢ ∀ (g : G), Hom.hom (actionDiagonalSucc G n).inv (g, f) = g • partialProd f
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
k G✝ : Type u
inst✝² : CommRing k
n✝ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n : ℕ
f✝ : Fin n → G
f : Fin Nat.zero → G
⊢ ∀ (g : G), Hom.hom (actionDiagonalSucc G Nat.zero).inv (g, f) = g • partialProd f
[PROOFSTEP]
intro g
[GOAL]
case zero
k G✝ : Type u
inst✝² : CommRing k
n✝ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n : ℕ
f✝ : Fin n → G
f : Fin Nat.zero → G
g : G
⊢ Hom.hom (actionDiagonalSucc G Nat.zero).inv (g, f) = g • partialProd f
[PROOFSTEP]
funext (x : Fin 1)
[GOAL]
case zero.h
k G✝ : Type u
inst✝² : CommRing k
n✝ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n : ℕ
f✝ : Fin n → G
f : Fin Nat.zero → G
g : G
x : Fin 1
⊢ Hom.hom (actionDiagonalSucc G Nat.zero).inv (g, f) x = (g • partialProd f) x
[PROOFSTEP]
simp only [Subsingleton.elim x 0, Pi.smul_apply, Fin.partialProd_zero, smul_eq_mul, mul_one]
[GOAL]
case zero.h
k G✝ : Type u
inst✝² : CommRing k
n✝ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n : ℕ
f✝ : Fin n → G
f : Fin Nat.zero → G
g : G
x : Fin 1
⊢ Hom.hom (actionDiagonalSucc G Nat.zero).inv (g, f) 0 = g
[PROOFSTEP]
rfl
[GOAL]
case succ
k G✝ : Type u
inst✝² : CommRing k
n✝¹ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n✝ : ℕ
f✝ : Fin n✝ → G
n : ℕ
hn : ∀ (f : Fin n → G) (g : G), Hom.hom (actionDiagonalSucc G n).inv (g, f) = g • partialProd f
f : Fin (Nat.succ n) → G
⊢ ∀ (g : G), Hom.hom (actionDiagonalSucc G (Nat.succ n)).inv (g, f) = g • partialProd f
[PROOFSTEP]
intro g
[GOAL]
case succ
k G✝ : Type u
inst✝² : CommRing k
n✝¹ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n✝ : ℕ
f✝ : Fin n✝ → G
n : ℕ
hn : ∀ (f : Fin n → G) (g : G), Hom.hom (actionDiagonalSucc G n).inv (g, f) = g • partialProd f
f : Fin (Nat.succ n) → G
g : G
⊢ Hom.hom (actionDiagonalSucc G (Nat.succ n)).inv (g, f) = g • partialProd f
[PROOFSTEP]
funext x
[GOAL]
case succ.h
k G✝ : Type u
inst✝² : CommRing k
n✝¹ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n✝ : ℕ
f✝ : Fin n✝ → G
n : ℕ
hn : ∀ (f : Fin n → G) (g : G), Hom.hom (actionDiagonalSucc G n).inv (g, f) = g • partialProd f
f : Fin (Nat.succ n) → G
g : G
x : Fin (Nat.succ n + 1)
⊢ Hom.hom (actionDiagonalSucc G (Nat.succ n)).inv (g, f) x = (g • partialProd f) x
[PROOFSTEP]
dsimp [actionDiagonalSucc]
[GOAL]
case succ.h
k G✝ : Type u
inst✝² : CommRing k
n✝¹ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n✝ : ℕ
f✝ : Fin n✝ → G
n : ℕ
hn : ∀ (f : Fin n → G) (g : G), Hom.hom (actionDiagonalSucc G n).inv (g, f) = g • partialProd f
f : Fin (Nat.succ n) → G
g : G
x : Fin (Nat.succ n + 1)
⊢ ↑(Equiv.piFinSuccAboveEquiv (fun a => G) 0).symm
      (g,
        Hom.hom (actionDiagonalSucc G n).inv
          (↑(FunctorCategoryEquivalence.inverse.obj
                  (FunctorCategoryEquivalence.functor.obj (leftRegular G) ⊗
                    FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 })).ρ
            g (↑(Equiv.piFinSuccAboveEquiv (fun x => G) 0) f)))
      x =
    g * partialProd f x
[PROOFSTEP]
erw [hn, Equiv.piFinSuccAboveEquiv_symm_apply]
[GOAL]
case succ.h
k G✝ : Type u
inst✝² : CommRing k
n✝¹ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n✝ : ℕ
f✝ : Fin n✝ → G
n : ℕ
hn : ∀ (f : Fin n → G) (g : G), Hom.hom (actionDiagonalSucc G n).inv (g, f) = g • partialProd f
f : Fin (Nat.succ n) → G
g : G
x : Fin (Nat.succ n + 1)
⊢ (fun f => Fin.insertNth 0 f.fst f.snd)
      (g,
        Limits.BinaryFan.fst
            (Limits.BinaryFan.mk
              (NatTrans.app
                  (Limits.Types.binaryProductLimitCone
                        ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                        ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                  { as := Limits.WalkingPair.left } ≫
                (FunctorCategoryEquivalence.functor.obj (leftRegular G)).map g)
              (NatTrans.app
                  (Limits.Types.binaryProductLimitCone
                        ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                        ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                  { as := Limits.WalkingPair.right } ≫
                (FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).map g))
            (↑(Equiv.piFinSuccAboveEquiv (fun x => G) 0) f) •
          partialProd
            (Limits.BinaryFan.snd
              (Limits.BinaryFan.mk
                (NatTrans.app
                    (Limits.Types.binaryProductLimitCone
                          ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                          ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                    { as := Limits.WalkingPair.left } ≫
                  (FunctorCategoryEquivalence.functor.obj (leftRegular G)).map g)
                (NatTrans.app
                    (Limits.Types.binaryProductLimitCone
                          ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                          ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                    { as := Limits.WalkingPair.right } ≫
                  (FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).map g))
              (↑(Equiv.piFinSuccAboveEquiv (fun x => G) 0) f)))
      x =
    g * partialProd f x
[PROOFSTEP]
refine' Fin.cases _ (fun i => _) x
[GOAL]
case succ.h.refine'_1
k G✝ : Type u
inst✝² : CommRing k
n✝¹ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n✝ : ℕ
f✝ : Fin n✝ → G
n : ℕ
hn : ∀ (f : Fin n → G) (g : G), Hom.hom (actionDiagonalSucc G n).inv (g, f) = g • partialProd f
f : Fin (Nat.succ n) → G
g : G
x : Fin (Nat.succ n + 1)
⊢ (fun f => Fin.insertNth 0 f.fst f.snd)
      (g,
        Limits.BinaryFan.fst
            (Limits.BinaryFan.mk
              (NatTrans.app
                  (Limits.Types.binaryProductLimitCone
                        ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                        ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                  { as := Limits.WalkingPair.left } ≫
                (FunctorCategoryEquivalence.functor.obj (leftRegular G)).map g)
              (NatTrans.app
                  (Limits.Types.binaryProductLimitCone
                        ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                        ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                  { as := Limits.WalkingPair.right } ≫
                (FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).map g))
            (↑(Equiv.piFinSuccAboveEquiv (fun x => G) 0) f) •
          partialProd
            (Limits.BinaryFan.snd
              (Limits.BinaryFan.mk
                (NatTrans.app
                    (Limits.Types.binaryProductLimitCone
                          ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                          ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                    { as := Limits.WalkingPair.left } ≫
                  (FunctorCategoryEquivalence.functor.obj (leftRegular G)).map g)
                (NatTrans.app
                    (Limits.Types.binaryProductLimitCone
                          ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                          ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                    { as := Limits.WalkingPair.right } ≫
                  (FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).map g))
              (↑(Equiv.piFinSuccAboveEquiv (fun x => G) 0) f)))
      0 =
    g * partialProd f 0
[PROOFSTEP]
simp only [Fin.insertNth_zero, Fin.cons_zero, Fin.partialProd_zero, mul_one]
[GOAL]
case succ.h.refine'_2
k G✝ : Type u
inst✝² : CommRing k
n✝¹ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n✝ : ℕ
f✝ : Fin n✝ → G
n : ℕ
hn : ∀ (f : Fin n → G) (g : G), Hom.hom (actionDiagonalSucc G n).inv (g, f) = g • partialProd f
f : Fin (Nat.succ n) → G
g : G
x : Fin (Nat.succ n + 1)
i : Fin (n + 1)
⊢ (fun f => Fin.insertNth 0 f.fst f.snd)
      (g,
        Limits.BinaryFan.fst
            (Limits.BinaryFan.mk
              (NatTrans.app
                  (Limits.Types.binaryProductLimitCone
                        ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                        ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                  { as := Limits.WalkingPair.left } ≫
                (FunctorCategoryEquivalence.functor.obj (leftRegular G)).map g)
              (NatTrans.app
                  (Limits.Types.binaryProductLimitCone
                        ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                        ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                  { as := Limits.WalkingPair.right } ≫
                (FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).map g))
            (↑(Equiv.piFinSuccAboveEquiv (fun x => G) 0) f) •
          partialProd
            (Limits.BinaryFan.snd
              (Limits.BinaryFan.mk
                (NatTrans.app
                    (Limits.Types.binaryProductLimitCone
                          ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                          ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                    { as := Limits.WalkingPair.left } ≫
                  (FunctorCategoryEquivalence.functor.obj (leftRegular G)).map g)
                (NatTrans.app
                    (Limits.Types.binaryProductLimitCone
                          ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                          ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                    { as := Limits.WalkingPair.right } ≫
                  (FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).map g))
              (↑(Equiv.piFinSuccAboveEquiv (fun x => G) 0) f)))
      (Fin.succ i) =
    g * partialProd f (Fin.succ i)
[PROOFSTEP]
simp only [Fin.cons_succ, Pi.smul_apply, smul_eq_mul, Fin.partialProd_succ', ← mul_assoc]
[GOAL]
case succ.h.refine'_2
k G✝ : Type u
inst✝² : CommRing k
n✝¹ : ℕ
inst✝¹ : Group G✝
G : Type u
inst✝ : Group G
n✝ : ℕ
f✝ : Fin n✝ → G
n : ℕ
hn : ∀ (f : Fin n → G) (g : G), Hom.hom (actionDiagonalSucc G n).inv (g, f) = g • partialProd f
f : Fin (Nat.succ n) → G
g : G
x : Fin (Nat.succ n + 1)
i : Fin (n + 1)
⊢ Fin.insertNth 0 g
      (Limits.BinaryFan.fst
          (Limits.BinaryFan.mk
            (NatTrans.app
                (Limits.Types.binaryProductLimitCone
                      ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                      ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                { as := Limits.WalkingPair.left } ≫
              (FunctorCategoryEquivalence.functor.obj (leftRegular G)).map g)
            (NatTrans.app
                (Limits.Types.binaryProductLimitCone
                      ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                      ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                { as := Limits.WalkingPair.right } ≫
              (FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).map g))
          (↑(Equiv.piFinSuccAboveEquiv (fun x => G) 0) f) •
        partialProd
          (Limits.BinaryFan.snd
            (Limits.BinaryFan.mk
              (NatTrans.app
                  (Limits.Types.binaryProductLimitCone
                        ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                        ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                  { as := Limits.WalkingPair.left } ≫
                (FunctorCategoryEquivalence.functor.obj (leftRegular G)).map g)
              (NatTrans.app
                  (Limits.Types.binaryProductLimitCone
                        ((FunctorCategoryEquivalence.functor.obj (leftRegular G)).obj PUnit.unit)
                        ((FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).obj PUnit.unit)).cone.π
                  { as := Limits.WalkingPair.right } ≫
                (FunctorCategoryEquivalence.functor.obj { V := Fin n → G, ρ := 1 }).map g))
            (↑(Equiv.piFinSuccAboveEquiv (fun x => G) 0) f)))
      (Fin.succ i) =
    g * f 0 * partialProd (Fin.tail f) i
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
f : Fin (n + 1) → G
a : k
⊢ ↑(diagonalSucc k G n).hom.hom (single f a) =
    single (f 0) 1 ⊗ₜ[k] single (fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i)) a
[PROOFSTEP]
change
  (𝟙 ((linearization k G).1.obj (Action.leftRegular G)).V ⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom)
      ((inv ((linearization k G).μ (Action.leftRegular G) { V := Fin n → G, ρ := 1 })).hom
        ((lmapDomain k k (actionDiagonalSucc G n).hom.hom) (single f a))) =
    _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
f : Fin (n + 1) → G
a : k
⊢ ↑(𝟙 ((linearization k G).toLaxMonoidalFunctor.toFunctor.obj (Action.leftRegular G)).V ⊗
          (linearizationTrivialIso k G (Fin n → G)).hom.hom)
      (↑(inv
              (LaxMonoidalFunctor.μ (linearization k G).toLaxMonoidalFunctor (Action.leftRegular G)
                { V := Fin n → G, ρ := 1 })).hom
        (↑(lmapDomain k k (actionDiagonalSucc G n).hom.hom) (single f a))) =
    single (f 0) 1 ⊗ₜ[k] single (fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i)) a
[PROOFSTEP]
simp only [CategoryTheory.Functor.map_id, linearization_μ_inv_hom]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
f : Fin (n + 1) → G
a : k
⊢ ↑(𝟙 ((linearization k G).toLaxMonoidalFunctor.toFunctor.obj (Action.leftRegular G)).V ⊗
          (linearizationTrivialIso k G (Fin n → G)).hom.hom)
      (↑↑(LinearEquiv.symm (finsuppTensorFinsupp' k (Action.leftRegular G).V (Fin n → G)))
        (↑(lmapDomain k k (actionDiagonalSucc G n).hom.hom) (single f a))) =
    single (f 0) 1 ⊗ₜ[k] single (fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i)) a
[PROOFSTEP]
rw [lmapDomain_apply, mapDomain_single, LinearEquiv.coe_toLinearMap, finsuppTensorFinsupp', LinearEquiv.trans_symm,
  LinearEquiv.trans_apply, lcongr_symm, Equiv.refl_symm]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
f : Fin (n + 1) → G
a : k
⊢ ↑(𝟙 ((linearization k G).toLaxMonoidalFunctor.toFunctor.obj (Action.leftRegular G)).V ⊗
          (linearizationTrivialIso k G (Fin n → G)).hom.hom)
      (↑(LinearEquiv.symm (finsuppTensorFinsupp k k k (Action.leftRegular G).V (Fin n → G)))
        (↑(lcongr (Equiv.refl ((Action.leftRegular G).V × (Fin n → G))) (LinearEquiv.symm (TensorProduct.lid k k)))
          (single (Action.Hom.hom (actionDiagonalSucc G n).hom f) a))) =
    single (f 0) 1 ⊗ₜ[k] single (fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i)) a
[PROOFSTEP]
erw [lcongr_single]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
f : Fin (n + 1) → G
a : k
⊢ ↑(𝟙 ((linearization k G).toLaxMonoidalFunctor.toFunctor.obj (Action.leftRegular G)).V ⊗
          (linearizationTrivialIso k G (Fin n → G)).hom.hom)
      (↑(LinearEquiv.symm (finsuppTensorFinsupp k k k (Action.leftRegular G).V (Fin n → G)))
        (single (↑(Equiv.refl ((Action.leftRegular G).V × (Fin n → G))) (Action.Hom.hom (actionDiagonalSucc G n).hom f))
          (↑(LinearEquiv.symm (TensorProduct.lid k k)) a))) =
    single (f 0) 1 ⊗ₜ[k] single (fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i)) a
[PROOFSTEP]
rw [TensorProduct.lid_symm_apply, actionDiagonalSucc_hom_apply, finsuppTensorFinsupp_symm_single]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
f : Fin (n + 1) → G
a : k
⊢ ↑(𝟙 ((linearization k G).toLaxMonoidalFunctor.toFunctor.obj (Action.leftRegular G)).V ⊗
          (linearizationTrivialIso k G (Fin n → G)).hom.hom)
      (single
          (↑(Equiv.refl ((Action.leftRegular G).V × (Fin n → G)))
              (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i))).fst
          1 ⊗ₜ[k]
        single
          (↑(Equiv.refl ((Action.leftRegular G).V × (Fin n → G)))
              (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i))).snd
          a) =
    single (f 0) 1 ⊗ₜ[k] single (fun i => (f (Fin.castSucc i))⁻¹ * f (Fin.succ i)) a
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : Fin n → G
a b : k
⊢ ↑(diagonalSucc k G n).inv.hom (single g a ⊗ₜ[k] single f b) = single (g • partialProd f) (a * b)
[PROOFSTEP]
change
  mapDomain (actionDiagonalSucc G n).inv.hom
      (lcongr (Equiv.refl (G × (Fin n → G))) (TensorProduct.lid k k)
        (finsuppTensorFinsupp k k k G (Fin n → G) (single g a ⊗ₜ[k] single f b))) =
    single (g • partialProd f) (a * b)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : Fin n → G
a b : k
⊢ mapDomain (actionDiagonalSucc G n).inv.hom
      (↑(lcongr (Equiv.refl (G × (Fin n → G))) (TensorProduct.lid k k))
        (↑(finsuppTensorFinsupp k k k G (Fin n → G)) (single g a ⊗ₜ[k] single f b))) =
    single (g • partialProd f) (a * b)
[PROOFSTEP]
rw [finsuppTensorFinsupp_single, lcongr_single, mapDomain_single, Equiv.refl_apply, actionDiagonalSucc_inv_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : Fin n → G
a b : k
⊢ single (g • partialProd f) (↑(TensorProduct.lid k k) (a ⊗ₜ[k] b)) = single (g • partialProd f) (a * b)
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : (Fin n → G) →₀ k
r : k
⊢ ↑(diagonalSucc k G n).inv.hom (single g r ⊗ₜ[k] f) =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) f
[PROOFSTEP]
refine'
  f.induction _
    _
      /- Porting note: broken proof was
        · simp only [TensorProduct.tmul_zero, map_zero]
        · intro a b x ha hb hx
          simp only [lift_apply, smul_single', mul_one, TensorProduct.tmul_add, map_add,
            diagonalSucc_inv_single_single, hx, Finsupp.sum_single_index, mul_comm b,
            zero_mul, single_zero] -/
[GOAL]
case refine'_1
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : (Fin n → G) →₀ k
r : k
⊢ ↑(diagonalSucc k G n).inv.hom (single g r ⊗ₜ[k] 0) =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) 0
[PROOFSTEP]
rw [TensorProduct.tmul_zero, map_zero, map_zero]
[GOAL]
case refine'_2
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : (Fin n → G) →₀ k
r : k
⊢ ∀ (a : Fin n → G) (b : k) (f : (Fin n → G) →₀ k),
    ¬a ∈ f.support →
      b ≠ 0 →
        ↑(diagonalSucc k G n).inv.hom (single g r ⊗ₜ[k] f) =
            ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) f →
          ↑(diagonalSucc k G n).inv.hom (single g r ⊗ₜ[k] (single a b + f)) =
            ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r)
              (single a b + f)
[PROOFSTEP]
intro _ _ _ _ _ hx
[GOAL]
case refine'_2
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : (Fin n → G) →₀ k
r : k
a✝² : Fin n → G
b✝ : k
f✝ : (Fin n → G) →₀ k
a✝¹ : ¬a✝² ∈ f✝.support
a✝ : b✝ ≠ 0
hx :
  ↑(diagonalSucc k G n).inv.hom (single g r ⊗ₜ[k] f✝) =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) f✝
⊢ ↑(diagonalSucc k G n).inv.hom (single g r ⊗ₜ[k] (single a✝² b✝ + f✝)) =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) (single a✝² b✝ + f✝)
[PROOFSTEP]
rw [TensorProduct.tmul_add, map_add, map_add, hx]
[GOAL]
case refine'_2
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : (Fin n → G) →₀ k
r : k
a✝² : Fin n → G
b✝ : k
f✝ : (Fin n → G) →₀ k
a✝¹ : ¬a✝² ∈ f✝.support
a✝ : b✝ ≠ 0
hx :
  ↑(diagonalSucc k G n).inv.hom (single g r ⊗ₜ[k] f✝) =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) f✝
⊢ ↑(diagonalSucc k G n).inv.hom (single g r ⊗ₜ[k] single a✝² b✝) +
      ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) f✝ =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) (single a✝² b✝) +
      ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) f✝
[PROOFSTEP]
simp_rw [lift_apply, smul_single, smul_eq_mul, diagonalSucc_inv_single_single]
[GOAL]
case refine'_2
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : (Fin n → G) →₀ k
r : k
a✝² : Fin n → G
b✝ : k
f✝ : (Fin n → G) →₀ k
a✝¹ : ¬a✝² ∈ f✝.support
a✝ : b✝ ≠ 0
hx :
  ↑(diagonalSucc k G n).inv.hom (single g r ⊗ₜ[k] f✝) =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) f✝
⊢ (single (g • partialProd a✝²) (r * b✝) + sum f✝ fun x r_1 => single (g • partialProd x) (r_1 * r)) =
    (sum (single a✝² b✝) fun x r_1 => single (g • partialProd x) (r_1 * r)) +
      sum f✝ fun x r_1 => single (g • partialProd x) (r_1 * r)
[PROOFSTEP]
rw [sum_single_index, mul_comm]
[GOAL]
case refine'_2
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : (Fin n → G) →₀ k
r : k
a✝² : Fin n → G
b✝ : k
f✝ : (Fin n → G) →₀ k
a✝¹ : ¬a✝² ∈ f✝.support
a✝ : b✝ ≠ 0
hx :
  ↑(diagonalSucc k G n).inv.hom (single g r ⊗ₜ[k] f✝) =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) f✝
⊢ single (g • partialProd a✝²) (0 * r) = 0
[PROOFSTEP]
rw [zero_mul, single_zero]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G →₀ k
f : Fin n → G
r : k
⊢ ↑(diagonalSucc k G n).inv.hom (g ⊗ₜ[k] single f r) =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) g
[PROOFSTEP]
refine'
  g.induction _
    _
      /- Porting note: broken proof was
        · simp only [TensorProduct.zero_tmul, map_zero]
        · intro a b x ha hb hx
          simp only [lift_apply, smul_single', map_add, hx, diagonalSucc_inv_single_single,
            TensorProduct.add_tmul, Finsupp.sum_single_index, zero_mul, single_zero] -/
[GOAL]
case refine'_1
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G →₀ k
f : Fin n → G
r : k
⊢ ↑(diagonalSucc k G n).inv.hom (0 ⊗ₜ[k] single f r) =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) 0
[PROOFSTEP]
rw [TensorProduct.zero_tmul, map_zero, map_zero]
[GOAL]
case refine'_2
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G →₀ k
f : Fin n → G
r : k
⊢ ∀ (a : G) (b : k) (f_1 : G →₀ k),
    ¬a ∈ f_1.support →
      b ≠ 0 →
        ↑(diagonalSucc k G n).inv.hom (f_1 ⊗ₜ[k] single f r) =
            ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) f_1 →
          ↑(diagonalSucc k G n).inv.hom ((single a b + f_1) ⊗ₜ[k] single f r) =
            ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) (single a b + f_1)
[PROOFSTEP]
intro _ _ _ _ _ hx
[GOAL]
case refine'_2
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G →₀ k
f : Fin n → G
r : k
a✝² : G
b✝ : k
f✝ : G →₀ k
a✝¹ : ¬a✝² ∈ f✝.support
a✝ : b✝ ≠ 0
hx :
  ↑(diagonalSucc k G n).inv.hom (f✝ ⊗ₜ[k] single f r) =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) f✝
⊢ ↑(diagonalSucc k G n).inv.hom ((single a✝² b✝ + f✝) ⊗ₜ[k] single f r) =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) (single a✝² b✝ + f✝)
[PROOFSTEP]
rw [TensorProduct.add_tmul, map_add, map_add, hx]
[GOAL]
case refine'_2
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G →₀ k
f : Fin n → G
r : k
a✝² : G
b✝ : k
f✝ : G →₀ k
a✝¹ : ¬a✝² ∈ f✝.support
a✝ : b✝ ≠ 0
hx :
  ↑(diagonalSucc k G n).inv.hom (f✝ ⊗ₜ[k] single f r) =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) f✝
⊢ ↑(diagonalSucc k G n).inv.hom (single a✝² b✝ ⊗ₜ[k] single f r) +
      ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) f✝ =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) (single a✝² b✝) +
      ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) f✝
[PROOFSTEP]
simp_rw [lift_apply, smul_single', diagonalSucc_inv_single_single]
[GOAL]
case refine'_2
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G →₀ k
f : Fin n → G
r : k
a✝² : G
b✝ : k
f✝ : G →₀ k
a✝¹ : ¬a✝² ∈ f✝.support
a✝ : b✝ ≠ 0
hx :
  ↑(diagonalSucc k G n).inv.hom (f✝ ⊗ₜ[k] single f r) =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) f✝
⊢ (single (a✝² • partialProd f) (b✝ * r) + sum f✝ fun x r_1 => single (x • partialProd f) (r_1 * r)) =
    (sum (single a✝² b✝) fun x r_1 => single (x • partialProd f) (r_1 * r)) +
      sum f✝ fun x r_1 => single (x • partialProd f) (r_1 * r)
[PROOFSTEP]
rw [sum_single_index]
[GOAL]
case refine'_2
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G →₀ k
f : Fin n → G
r : k
a✝² : G
b✝ : k
f✝ : G →₀ k
a✝¹ : ¬a✝² ∈ f✝.support
a✝ : b✝ ≠ 0
hx :
  ↑(diagonalSucc k G n).inv.hom (f✝ ⊗ₜ[k] single f r) =
    ↑(↑(Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) f✝
⊢ single (a✝² • partialProd f) (0 * r) = 0
[PROOFSTEP]
rw [zero_mul, single_zero]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
src✝ : ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj
      (Rep.leftRegular k G ⊗ Rep.trivial k G ((Fin n → G) →₀ k))) ≃ₗ[MonoidAlgebra k G]
  ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj (Rep.diagonal k G (n + 1))) :=
  Iso.toLinearEquiv (Rep.equivalenceModuleMonoidAlgebra.functor.mapIso (diagonalSucc k G n).symm)
r : MonoidAlgebra k G
x : MonoidAlgebra k G ⊗[k] ((Fin n → G) →₀ k)
⊢ AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id (MonoidAlgebra k G)) r • AddHom.toFun src✝.toAddHom x
[PROOFSTEP]
rw [RingHom.id_apply, LinearEquiv.toFun_eq_coe, ← LinearEquiv.map_smul]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
src✝ : ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj
      (Rep.leftRegular k G ⊗ Rep.trivial k G ((Fin n → G) →₀ k))) ≃ₗ[MonoidAlgebra k G]
  ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj (Rep.diagonal k G (n + 1))) :=
  Iso.toLinearEquiv (Rep.equivalenceModuleMonoidAlgebra.functor.mapIso (diagonalSucc k G n).symm)
r : MonoidAlgebra k G
x : MonoidAlgebra k G ⊗[k] ((Fin n → G) →₀ k)
⊢ ↑src✝ (r • x) = ↑src✝ (r • x)
[PROOFSTEP]
congr 1
  /- Porting note: broken proof was
        refine' x.induction_on _ (fun x y => _) fun y z hy hz => _
        · simp only [smul_zero]
        · simp only [TensorProduct.smul_tmul']
          show (r * x) ⊗ₜ y = _
          rw [← ofMulAction_self_smul_eq_mul, smul_tprod_one_asModule]
        · rw [smul_add, hz, hy, smul_add] -/
[GOAL]
case h.e_6.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
src✝ : ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj
      (Rep.leftRegular k G ⊗ Rep.trivial k G ((Fin n → G) →₀ k))) ≃ₗ[MonoidAlgebra k G]
  ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj (Rep.diagonal k G (n + 1))) :=
  Iso.toLinearEquiv (Rep.equivalenceModuleMonoidAlgebra.functor.mapIso (diagonalSucc k G n).symm)
r : MonoidAlgebra k G
x : MonoidAlgebra k G ⊗[k] ((Fin n → G) →₀ k)
⊢ r • x = r • x
[PROOFSTEP]
show _ = Representation.asAlgebraHom (tensorObj (Rep.leftRegular k G) (Rep.trivial k G ((Fin n → G) →₀ k))).ρ r _
[GOAL]
case h.e_6.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
src✝ : ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj
      (Rep.leftRegular k G ⊗ Rep.trivial k G ((Fin n → G) →₀ k))) ≃ₗ[MonoidAlgebra k G]
  ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj (Rep.diagonal k G (n + 1))) :=
  Iso.toLinearEquiv (Rep.equivalenceModuleMonoidAlgebra.functor.mapIso (diagonalSucc k G n).symm)
r : MonoidAlgebra k G
x : MonoidAlgebra k G ⊗[k] ((Fin n → G) →₀ k)
⊢ r • x = ↑(↑(asAlgebraHom (Rep.ρ (Rep.leftRegular k G ⊗ Rep.trivial k G ((Fin n → G) →₀ k)))) r) x
[PROOFSTEP]
refine' x.induction_on _ (fun x y => _) fun y z hy hz => _
[GOAL]
case h.e_6.h.refine'_1
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
src✝ : ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj
      (Rep.leftRegular k G ⊗ Rep.trivial k G ((Fin n → G) →₀ k))) ≃ₗ[MonoidAlgebra k G]
  ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj (Rep.diagonal k G (n + 1))) :=
  Iso.toLinearEquiv (Rep.equivalenceModuleMonoidAlgebra.functor.mapIso (diagonalSucc k G n).symm)
r : MonoidAlgebra k G
x : MonoidAlgebra k G ⊗[k] ((Fin n → G) →₀ k)
⊢ r • 0 = ↑(↑(asAlgebraHom (Rep.ρ (Rep.leftRegular k G ⊗ Rep.trivial k G ((Fin n → G) →₀ k)))) r) 0
[PROOFSTEP]
rw [smul_zero, map_zero]
[GOAL]
case h.e_6.h.refine'_2
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
src✝ : ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj
      (Rep.leftRegular k G ⊗ Rep.trivial k G ((Fin n → G) →₀ k))) ≃ₗ[MonoidAlgebra k G]
  ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj (Rep.diagonal k G (n + 1))) :=
  Iso.toLinearEquiv (Rep.equivalenceModuleMonoidAlgebra.functor.mapIso (diagonalSucc k G n).symm)
r : MonoidAlgebra k G
x✝ : MonoidAlgebra k G ⊗[k] ((Fin n → G) →₀ k)
x : MonoidAlgebra k G
y : (Fin n → G) →₀ k
⊢ r • x ⊗ₜ[k] y = ↑(↑(asAlgebraHom (Rep.ρ (Rep.leftRegular k G ⊗ Rep.trivial k G ((Fin n → G) →₀ k)))) r) (x ⊗ₜ[k] y)
[PROOFSTEP]
rw [TensorProduct.smul_tmul', smul_eq_mul, ← ofMulAction_self_smul_eq_mul]
[GOAL]
case h.e_6.h.refine'_2
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
src✝ : ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj
      (Rep.leftRegular k G ⊗ Rep.trivial k G ((Fin n → G) →₀ k))) ≃ₗ[MonoidAlgebra k G]
  ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj (Rep.diagonal k G (n + 1))) :=
  Iso.toLinearEquiv (Rep.equivalenceModuleMonoidAlgebra.functor.mapIso (diagonalSucc k G n).symm)
r : MonoidAlgebra k G
x✝ : MonoidAlgebra k G ⊗[k] ((Fin n → G) →₀ k)
x : MonoidAlgebra k G
y : (Fin n → G) →₀ k
⊢ (r • x) ⊗ₜ[k] y = ↑(↑(asAlgebraHom (Rep.ρ (Rep.leftRegular k G ⊗ Rep.trivial k G ((Fin n → G) →₀ k)))) r) (x ⊗ₜ[k] y)
[PROOFSTEP]
exact (smul_tprod_one_asModule (Representation.ofMulAction k G G) r x y).symm
[GOAL]
case h.e_6.h.refine'_3
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
src✝ : ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj
      (Rep.leftRegular k G ⊗ Rep.trivial k G ((Fin n → G) →₀ k))) ≃ₗ[MonoidAlgebra k G]
  ↑(Rep.equivalenceModuleMonoidAlgebra.functor.obj (Rep.diagonal k G (n + 1))) :=
  Iso.toLinearEquiv (Rep.equivalenceModuleMonoidAlgebra.functor.mapIso (diagonalSucc k G n).symm)
r : MonoidAlgebra k G
x y z : MonoidAlgebra k G ⊗[k] ((Fin n → G) →₀ k)
hy : r • y = ↑(↑(asAlgebraHom (Rep.ρ (Rep.leftRegular k G ⊗ Rep.trivial k G ((Fin n → G) →₀ k)))) r) y
hz : r • z = ↑(↑(asAlgebraHom (Rep.ρ (Rep.leftRegular k G ⊗ Rep.trivial k G ((Fin n → G) →₀ k)))) r) z
⊢ r • (y + z) = ↑(↑(asAlgebraHom (Rep.ρ (Rep.leftRegular k G ⊗ Rep.trivial k G ((Fin n → G) →₀ k)))) r) (y + z)
[PROOFSTEP]
rw [smul_add, hz, hy, map_add]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : ofMulAction k G (Fin (n + 1) → G) ⟶ A
x : Fin n → G
⊢ ↑(diagonalHomEquiv n A) f x = ↑f.hom (Finsupp.single (Fin.partialProd x) 1)
[PROOFSTEP]
change f.hom ((diagonalSucc k G n).inv.hom (Finsupp.single 1 1 ⊗ₜ[k] Finsupp.single x 1)) = _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : ofMulAction k G (Fin (n + 1) → G) ⟶ A
x : Fin n → G
⊢ ↑f.hom (↑(diagonalSucc k G n).inv.hom (Finsupp.single 1 1 ⊗ₜ[k] Finsupp.single x 1)) =
    ↑f.hom (Finsupp.single (Fin.partialProd x) 1)
[PROOFSTEP]
rw [diagonalSucc_inv_single_single, one_smul, one_mul]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom (Finsupp.single x 1) =
    ↑(↑(ρ A) (x 0)) (f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i))
[PROOFSTEP]
unfold diagonalHomEquiv
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ ↑(↑(LinearEquiv.symm
                (LinearEquiv.trans
                  (LinearEquiv.trans
                    (Linear.homCongr k
                      (diagonalSucc k G n ≪≫ Representation.repOfTprodIso (Representation.ofMulAction k G G) 1)
                      (Iso.refl A))
                    (LinearEquiv.trans
                      (MonoidalClosed.linearHomEquivComm (of (Representation.ofMulAction k G G)) (of 1) A)
                      (leftRegularHomEquiv ((ihom (of 1)).obj A))))
                  (LinearEquiv.symm (Finsupp.llift (CoeSort.coe A) k k (Fin n → G)))))
            f).hom
      (Finsupp.single x 1) =
    ↑(↑(ρ A) (x 0)) (f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i))
[PROOFSTEP]
simp only [LinearEquiv.trans_symm, LinearEquiv.symm_symm, LinearEquiv.trans_apply, leftRegularHomEquiv_symm_apply,
  Linear.homCongr_symm_apply, Iso.trans_hom, Iso.refl_inv, Category.comp_id, Action.comp_hom,
  MonoidalClosed.linearHomEquivComm_symm_hom]
  -- Porting note: This is a sure sign that coercions for morphisms in `ModuleCat`
    -- are still not set up properly.
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ ↑(((diagonalSucc k G n).hom.hom ≫ (Representation.repOfTprodIso (Representation.ofMulAction k G G) 1).hom.hom) ≫
          ↑(TensorProduct.uncurry k (CoeSort.coe (of (Representation.ofMulAction k G G))) (CoeSort.coe (of 1))
                (CoeSort.coe A))
            (leftRegularHom ((ihom (of 1)).obj A) (↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f)).hom)
      (Finsupp.single x 1) =
    ↑(↑(ρ A) (x 0)) (f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i))
[PROOFSTEP]
rw [ModuleCat.coe_comp]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ (↑(↑(TensorProduct.uncurry k (CoeSort.coe (of (Representation.ofMulAction k G G))) (CoeSort.coe (of 1))
                (CoeSort.coe A))
            (leftRegularHom ((ihom (of 1)).obj A) (↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f)).hom) ∘
        ↑((diagonalSucc k G n).hom.hom ≫ (Representation.repOfTprodIso (Representation.ofMulAction k G G) 1).hom.hom))
      (Finsupp.single x 1) =
    ↑(↑(ρ A) (x 0)) (f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i))
[PROOFSTEP]
simp only [ModuleCat.coe_comp, Function.comp_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ ↑(↑(TensorProduct.uncurry k (CoeSort.coe (of (Representation.ofMulAction k G G))) (CoeSort.coe (of 1))
              (CoeSort.coe A))
          (leftRegularHom ((ihom (of 1)).obj A) (↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f)).hom)
      (↑(Representation.repOfTprodIso (Representation.ofMulAction k G G) 1).hom.hom
        (↑(diagonalSucc k G n).hom.hom (Finsupp.single x 1))) =
    ↑(↑(ρ A) (x 0)) (f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i))
[PROOFSTEP]
rw [diagonalSucc_hom_single]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ ↑(↑(TensorProduct.uncurry k (CoeSort.coe (of (Representation.ofMulAction k G G))) (CoeSort.coe (of 1))
              (CoeSort.coe A))
          (leftRegularHom ((ihom (of 1)).obj A) (↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f)).hom)
      (↑(Representation.repOfTprodIso (Representation.ofMulAction k G G) 1).hom.hom
        (Finsupp.single (x 0) 1 ⊗ₜ[k] Finsupp.single (fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i)) 1)) =
    ↑(↑(ρ A) (x 0)) (f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i))
[PROOFSTEP]
erw [TensorProduct.uncurry_apply, Finsupp.lift_apply, Finsupp.sum_single_index]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ ↑(1 • ↑(↑(ρ ((ihom (of 1)).obj A)) (x 0)) (↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f))
      (Finsupp.single (fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i)) 1) =
    ↑(↑(ρ A) (x 0)) (f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i))
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ 0 • ↑(↑(ρ ((ihom (of 1)).obj A)) (x 0)) (↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f) = 0
[PROOFSTEP]
simp only [one_smul]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ ↑(↑(↑(ρ ((ihom (of 1)).obj A)) (x 0)) (↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f))
      (Finsupp.single (fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i)) 1) =
    ↑(↑(ρ A) (x 0)) (f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i))
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ 0 • ↑(↑(ρ ((ihom (of 1)).obj A)) (x 0)) (↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f) = 0
[PROOFSTEP]
erw [Representation.linHom_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ ↑(LinearMap.comp (↑(ρ A) (x 0))
          (LinearMap.comp (↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f) (↑(ρ (of 1)) (x 0)⁻¹)))
      (Finsupp.single (fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i)) 1) =
    ↑(↑(ρ A) (x 0)) (f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i))
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ 0 • ↑(↑(ρ ((ihom (of 1)).obj A)) (x 0)) (↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f) = 0
[PROOFSTEP]
simp only [LinearMap.comp_apply, MonoidHom.one_apply, LinearMap.one_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ ↑(↑(ρ A) (x 0))
      (↑(↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f)
        (↑(↑(ρ (of 1)) (x 0)⁻¹) (Finsupp.single (fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i)) 1))) =
    ↑(↑(ρ A) (x 0)) (f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i))
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ 0 • ↑(↑(ρ ((ihom (of 1)).obj A)) (x 0)) (↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f) = 0
[PROOFSTEP]
erw [Finsupp.llift_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ ↑(↑(ρ A) (x 0))
      (↑(↑(Finsupp.lift (CoeSort.coe A) k (Fin n → G)) f)
        (↑(↑(ρ (of 1)) (x 0)⁻¹) (Finsupp.single (fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i)) 1))) =
    ↑(↑(ρ A) (x 0)) (f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i))
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ 0 • ↑(↑(ρ ((ihom (of 1)).obj A)) (x 0)) (↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f) = 0
[PROOFSTEP]
rw [Finsupp.lift_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ ↑(↑(ρ A) (x 0))
      (Finsupp.sum (↑(↑(ρ (of 1)) (x 0)⁻¹) (Finsupp.single (fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i)) 1))
        fun x r => r • f x) =
    ↑(↑(ρ A) (x 0)) (f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i))
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ 0 • ↑(↑(ρ ((ihom (of 1)).obj A)) (x 0)) (↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f) = 0
[PROOFSTEP]
erw [Finsupp.sum_single_index]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ ↑(↑(ρ A) (x 0)) (1 • f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i)) =
    ↑(↑(ρ A) (x 0)) (f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i))
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ (0 • f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i)) = 0
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ 0 • ↑(↑(ρ ((ihom (of 1)).obj A)) (x 0)) (↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f) = 0
[PROOFSTEP]
rw [one_smul]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ (0 • f fun i => (x (Fin.castSucc i))⁻¹ * x (Fin.succ i)) = 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ 0 • ↑(↑(ρ ((ihom (of 1)).obj A)) (x 0)) (↑(Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f) = 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
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 : Fin (n + 1)
⊢ ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom
      (Finsupp.single (Fin.partialProd g ∘ Fin.succAbove (Fin.succ a)) 1) =
    f (Fin.contractNth a (fun x x_1 => x * x_1) g)
[PROOFSTEP]
simp only [diagonalHomEquiv_symm_apply, Function.comp_apply, Fin.succ_succAbove_zero, Fin.partialProd_zero, map_one,
  Fin.succ_succAbove_succ, LinearMap.one_apply, Fin.partialProd_succ]
[GOAL]
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 : Fin (n + 1)
⊢ (f fun i =>
      (Fin.partialProd g (Fin.succAbove (Fin.succ a) (Fin.castSucc i)))⁻¹ *
        (Fin.partialProd g (Fin.castSucc (Fin.succAbove a i)) * g (Fin.succAbove a i))) =
    f (Fin.contractNth a (fun x x_1 => x * x_1) g)
[PROOFSTEP]
congr
[GOAL]
case e_a
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 : Fin (n + 1)
⊢ (fun i =>
      (Fin.partialProd g (Fin.succAbove (Fin.succ a) (Fin.castSucc i)))⁻¹ *
        (Fin.partialProd g (Fin.castSucc (Fin.succAbove a i)) * g (Fin.succAbove a i))) =
    Fin.contractNth a (fun x x_1 => x * x_1) g
[PROOFSTEP]
ext
[GOAL]
case 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
a : Fin (n + 1)
x✝ : Fin n
⊢ (Fin.partialProd g (Fin.succAbove (Fin.succ a) (Fin.castSucc x✝)))⁻¹ *
      (Fin.partialProd g (Fin.castSucc (Fin.succAbove a x✝)) * g (Fin.succAbove a x✝)) =
    Fin.contractNth a (fun x x_1 => x * x_1) g x✝
[PROOFSTEP]
rw [← Fin.partialProd_succ, Fin.inv_partialProd_mul_eq_contractNth]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
X✝ Y✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
⊢ (cechNerveTerminalFrom (Action.ofMulAction G G)).map f ≫
      ((fun n => limit.isoLimitCone (Action.ofMulActionLimitCone G fun x => G)) Y✝).hom =
    ((fun n => limit.isoLimitCone (Action.ofMulActionLimitCone G fun x => G)) X✝).hom ≫
      (classifyingSpaceUniversalCover G).map f
[PROOFSTEP]
refine' IsLimit.hom_ext (Action.ofMulActionLimitCone.{u, 0} G fun _ => G).2 fun j => _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
X✝ Y✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
j : Discrete (Fin (SimplexCategory.len Y✝.unop + 1))
⊢ ((cechNerveTerminalFrom (Action.ofMulAction G G)).map f ≫
        ((fun n => limit.isoLimitCone (Action.ofMulActionLimitCone G fun x => G)) Y✝).hom) ≫
      NatTrans.app (Action.ofMulActionLimitCone G fun x => G).cone.π j =
    (((fun n => limit.isoLimitCone (Action.ofMulActionLimitCone G fun x => G)) X✝).hom ≫
        (classifyingSpaceUniversalCover G).map f) ≫
      NatTrans.app (Action.ofMulActionLimitCone G fun x => G).cone.π j
[PROOFSTEP]
dsimp only [cechNerveTerminalFrom, Pi.lift]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
X✝ Y✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
j : Discrete (Fin (SimplexCategory.len Y✝.unop + 1))
⊢ (limit.lift (Discrete.functor fun b => Action.ofMulAction G G)
          (Fan.mk (∏ fun x => Action.ofMulAction G G) fun i =>
            Pi.π (fun x => Action.ofMulAction G G) (↑(SimplexCategory.Hom.toOrderHom f.unop) i)) ≫
        (limit.isoLimitCone (Action.ofMulActionLimitCone G fun x => G)).hom) ≫
      NatTrans.app (Action.ofMulActionLimitCone G fun x => G).cone.π j =
    ((limit.isoLimitCone (Action.ofMulActionLimitCone G fun x => G)).hom ≫ (classifyingSpaceUniversalCover G).map f) ≫
      NatTrans.app (Action.ofMulActionLimitCone G fun x => G).cone.π j
[PROOFSTEP]
rw [Category.assoc, limit.isoLimitCone_hom_π, limit.lift_π, Category.assoc]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
X✝ Y✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
j : Discrete (Fin (SimplexCategory.len Y✝.unop + 1))
⊢ NatTrans.app
      (Fan.mk (∏ fun x => Action.ofMulAction G G) fun i =>
          Pi.π (fun x => Action.ofMulAction G G) (↑(SimplexCategory.Hom.toOrderHom f.unop) i)).π
      j =
    (limit.isoLimitCone (Action.ofMulActionLimitCone G fun x => G)).hom ≫
      (classifyingSpaceUniversalCover G).map f ≫ NatTrans.app (Action.ofMulActionLimitCone G fun x => G).cone.π j
[PROOFSTEP]
exact (limit.isoLimitCone_hom_π _ _).symm
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ ExtraDegeneracy (compForgetAugmented G)
[PROOFSTEP]
refine'
  ExtraDegeneracy.ofIso (_ : (Arrow.mk <| terminal.from G).augmentedCechNerve ≅ _) (extraDegeneracyAugmentedCechNerve G)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ Arrow.augmentedCechNerve (mk (terminal.from G)) ≅ compForgetAugmented G
[PROOFSTEP]
exact
  Comma.isoMk (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G) (Iso.refl _)
    (by ext : 1; exact IsTerminal.hom_ext terminalIsTerminal _ _)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (𝟭 (SimplicialObject (Type u))).map (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G).hom ≫
      (compForgetAugmented G).hom =
    (Arrow.augmentedCechNerve (mk (terminal.from G))).hom ≫
      (const (Type u)).map (Iso.refl (Arrow.augmentedCechNerve (mk (terminal.from G))).right).hom
[PROOFSTEP]
ext : 1
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
n✝ : SimplexCategoryᵒᵖ
⊢ NatTrans.app
      ((𝟭 (SimplicialObject (Type u))).map (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G).hom ≫
        (compForgetAugmented G).hom)
      n✝ =
    NatTrans.app
      ((Arrow.augmentedCechNerve (mk (terminal.from G))).hom ≫
        (const (Type u)).map (Iso.refl (Arrow.augmentedCechNerve (mk (terminal.from G))).right).hom)
      n✝
[PROOFSTEP]
exact IsTerminal.hom_ext terminalIsTerminal _ _
[GOAL]
k G✝ : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G✝
G : Type u
n : ℕ
c : Fin (n + 1) → G
⊢ ↑(d k G n) (Finsupp.single c 1) = Finset.sum Finset.univ fun p => Finsupp.single (c ∘ Fin.succAbove p) ((-1) ^ ↑p)
[PROOFSTEP]
simp [d]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
⊢ (HomologicalComplex.d (resolution k G) (n + 1) n).hom = d k G (n + 1)
[PROOFSTEP]
refine' Finsupp.lhom_ext' fun x => LinearMap.ext_ring _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
⊢ ↑(LinearMap.comp (HomologicalComplex.d (resolution k G) (n + 1) n).hom (Finsupp.lsingle x)) 1 =
    ↑(LinearMap.comp (d k G (n + 1)) (Finsupp.lsingle x)) 1
[PROOFSTEP]
dsimp [GroupCohomology.resolution]
  /- Porting note: broken proof was
    simpa [← @intCast_smul k, simplicial_object.δ] -/
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
⊢ ↑(HomologicalComplex.d
            ((alternatingFaceMapComplex (Rep k G)).obj
              (classifyingSpaceUniversalCover G ⋙ (Rep.linearization k G).toLaxMonoidalFunctor.toFunctor))
            (n + 1) n).hom
      (Finsupp.single x 1) =
    ↑(d k G (n + 1)) (Finsupp.single x 1)
[PROOFSTEP]
simp_rw [alternatingFaceMapComplex_obj_d, AlternatingFaceMapComplex.objD, SimplicialObject.δ, Functor.comp_map, ←
  intCast_smul (k := k) ((-1) ^ _ : ℤ), Int.cast_pow, Int.cast_neg, Int.cast_one, Action.sum_hom, Action.smul_hom,
  Rep.linearization_map_hom]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
⊢ ↑(Finset.sum Finset.univ fun x =>
          (-1) ^ ↑x • Finsupp.lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x).op).hom)
      (Finsupp.single x 1) =
    ↑(d k G (n + 1)) (Finsupp.single x 1)
[PROOFSTEP]
rw [LinearMap.coeFn_sum, Fintype.sum_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
⊢ (Finset.sum Finset.univ fun c =>
      ↑((-1) ^ ↑c • Finsupp.lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ c).op).hom)
        (Finsupp.single x 1)) =
    ↑(d k G (n + 1)) (Finsupp.single x 1)
[PROOFSTEP]
erw [d_of (k := k) x]
  /- Porting note: want to rewrite `LinearMap.smul_apply` but simp/simp_rw won't do it; I need erw,
  so using Finset.sum_congr to get rid of the binder -/
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
⊢ (Finset.sum Finset.univ fun c =>
      ↑((-1) ^ ↑c • Finsupp.lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ c).op).hom)
        (Finsupp.single x 1)) =
    Finset.sum Finset.univ fun p => Finsupp.single (x ∘ Fin.succAbove p) ((-1) ^ ↑p)
[PROOFSTEP]
refine' Finset.sum_congr rfl fun _ _ => _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ ↑((-1) ^ ↑x✝¹ • Finsupp.lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x✝¹).op).hom)
      (Finsupp.single x 1) =
    Finsupp.single (x ∘ Fin.succAbove x✝¹) ((-1) ^ ↑x✝¹)
[PROOFSTEP]
erw [LinearMap.smul_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ (-1) ^ ↑x✝¹ •
      ↑(Finsupp.lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x✝¹).op).hom)
        (Finsupp.single x 1) =
    Finsupp.single (x ∘ Fin.succAbove x✝¹) ((-1) ^ ↑x✝¹)
[PROOFSTEP]
rw [Finsupp.lmapDomain_apply, Finsupp.mapDomain_single, Finsupp.smul_single', mul_one]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ Finsupp.single (Action.Hom.hom ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x✝¹).op) x) ((-1) ^ ↑x✝¹) =
    Finsupp.single (x ∘ Fin.succAbove x✝¹) ((-1) ^ ↑x✝¹)
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
g : ↑(MonCat.of G)
x✝ : Fin 1 → G
⊢ ↑(LinearMap.comp
          (↑(Rep.ofMulAction k G (Fin 1 → G)).ρ g ≫ Finsupp.total (Fin 1 → G) (↑(Rep.trivial k G k).V) k fun x => 1)
          (Finsupp.lsingle x✝))
      1 =
    ↑(LinearMap.comp ((Finsupp.total (Fin 1 → G) (↑(Rep.trivial k G k).V) k fun x => 1) ≫ ↑(Rep.trivial k G k).ρ g)
          (Finsupp.lsingle x✝))
      1
[PROOFSTEP]
show
  Finsupp.total (Fin 1 → G) k k (fun _ => (1 : k)) (Finsupp.mapDomain _ (Finsupp.single _ _)) =
    Finsupp.total (Fin 1 → G) k k (fun _ => (1 : k)) (Finsupp.single _ _)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
g : ↑(MonCat.of G)
x✝ : Fin 1 → G
⊢ ↑(Finsupp.total (Fin 1 → G) k k fun x => 1)
      (Finsupp.mapDomain (fun a => (fun x x_1 => x • x_1) g a) (Finsupp.single x✝ 1)) =
    ↑(Finsupp.total (Fin 1 → G) k k fun x => 1) (Finsupp.single x✝ 1)
[PROOFSTEP]
simp only [Finsupp.mapDomain_single, Finsupp.total_single]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ HomologicalComplex.Hom.f (forget₂ToModuleCatHomotopyEquiv k G).hom 0 = (forget₂ (Rep k G) (ModuleCat k)).map (ε k G)
[PROOFSTEP]
show (HomotopyEquiv.hom _ ≫ HomotopyEquiv.hom _ ≫ HomotopyEquiv.hom _).f 0 = _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ HomologicalComplex.Hom.f
      ((HomotopyEquiv.ofIso (compForgetAugmentedIso k G).symm).hom ≫
        (SimplicialObject.Augmented.ExtraDegeneracy.homotopyEquiv
              (extraDegeneracyCompForgetAugmentedToModule k G)).hom ≫
          (HomotopyEquiv.ofIso
              ((ChainComplex.single₀ (ModuleCat k)).mapIso
                (LinearEquiv.toModuleIso (Finsupp.LinearEquiv.finsuppUnique k k (⊤_ Type u))))).hom)
      0 =
    (forget₂ (Rep k G) (ModuleCat k)).map (ε k G)
[PROOFSTEP]
simp only [HomologicalComplex.comp_f]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ HomologicalComplex.Hom.f (HomotopyEquiv.ofIso (compForgetAugmentedIso k G).symm).hom 0 ≫
      HomologicalComplex.Hom.f
          (SimplicialObject.Augmented.ExtraDegeneracy.homotopyEquiv
              (extraDegeneracyCompForgetAugmentedToModule k G)).hom
          0 ≫
        HomologicalComplex.Hom.f
          (HomotopyEquiv.ofIso
              ((ChainComplex.single₀ (ModuleCat k)).mapIso
                (LinearEquiv.toModuleIso (Finsupp.LinearEquiv.finsuppUnique k k (⊤_ Type u))))).hom
          0 =
    (forget₂ (Rep k G) (ModuleCat k)).map (ε k G)
[PROOFSTEP]
dsimp
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ HomologicalComplex.Hom.f (HomotopyEquiv.ofIso (compForgetAugmentedIso k G).symm).hom 0 ≫
      HomologicalComplex.Hom.f
          (SimplicialObject.Augmented.ExtraDegeneracy.homotopyEquiv
              (extraDegeneracyCompForgetAugmentedToModule k G)).hom
          0 ≫
        HomologicalComplex.Hom.f
          (HomotopyEquiv.ofIso
              ((ChainComplex.single₀ (ModuleCat k)).mapIso
                (LinearEquiv.toModuleIso (Finsupp.LinearEquiv.finsuppUnique k k (⊤_ Type u))))).hom
          0 =
    (forget₂ (Rep k G) (ModuleCat k)).map (ε k G)
[PROOFSTEP]
convert Category.id_comp (X := (forget₂ToModuleCat k G).X 0) _
[GOAL]
case h.e'_2.h.e'_6.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
e_4✝ :
  (compForgetAugmented.toModule k G).left.obj (Opposite.op (SimplexCategory.mk 0)) =
    HomologicalComplex.X (forget₂ToModuleCat k G) 0
⊢ HomologicalComplex.Hom.f (HomotopyEquiv.ofIso (compForgetAugmentedIso k G).symm).hom 0 =
    𝟙 (HomologicalComplex.X (forget₂ToModuleCat k G) 0)
[PROOFSTEP]
dsimp only [HomotopyEquiv.ofIso, compForgetAugmentedIso, map_alternatingFaceMapComplex]
[GOAL]
case h.e'_2.h.e'_6.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
e_4✝ :
  (compForgetAugmented.toModule k G).left.obj (Opposite.op (SimplexCategory.mk 0)) =
    HomologicalComplex.X (forget₂ToModuleCat k G) 0
⊢ HomologicalComplex.Hom.f
      (eqToIso
            (_ :
              ((SimplicialObject.whiskering (Rep k G) (ModuleCat k)).obj (forget₂ (Rep k G) (ModuleCat k)) ⋙
                      alternatingFaceMapComplex (ModuleCat k)).obj
                  (classifyingSpaceUniversalCover G ⋙ (Rep.linearization k G).toLaxMonoidalFunctor.toFunctor) =
                (alternatingFaceMapComplex (Rep k G) ⋙
                      Functor.mapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)).obj
                  (classifyingSpaceUniversalCover G ⋙ (Rep.linearization k G).toLaxMonoidalFunctor.toFunctor))).symm.hom
      0 =
    𝟙 (HomologicalComplex.X (forget₂ToModuleCat k G) 0)
[PROOFSTEP]
simp only [Iso.symm_hom, eqToIso.inv, HomologicalComplex.eqToHom_f, eqToHom_refl]
[GOAL]
case h.e'_3
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (forget₂ (Rep k G) (ModuleCat k)).map (ε k G) =
    HomologicalComplex.Hom.f
        (SimplicialObject.Augmented.ExtraDegeneracy.homotopyEquiv (extraDegeneracyCompForgetAugmentedToModule k G)).hom
        0 ≫
      HomologicalComplex.Hom.f
        (HomotopyEquiv.ofIso
            ((ChainComplex.single₀ (ModuleCat k)).mapIso
              (LinearEquiv.toModuleIso (Finsupp.LinearEquiv.finsuppUnique k k (⊤_ Type u))))).hom
        0
[PROOFSTEP]
trans (Finsupp.total _ _ _ fun _ => (1 : k)).comp ((ModuleCat.free k).map (terminal.from _))
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (forget₂ (Rep k G) (ModuleCat k)).map (ε k G) =
    LinearMap.comp (Finsupp.total (⊤_ Type u) k k fun x => 1) ((ModuleCat.free k).map (terminal.from (Fin 1 → G)))
[PROOFSTEP]
dsimp
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (forget₂ (Rep k G) (ModuleCat k)).map (ε k G) =
    LinearMap.comp (Finsupp.total (⊤_ Type u) k k fun x => 1) (Finsupp.lmapDomain k k (terminal.from (Fin 1 → G)))
[PROOFSTEP]
erw [Finsupp.lmapDomain_total (α := Fin 1 → G) (R := k) (α' := ⊤_ Type u) (v := fun _ => (1 : k)) (v' := fun _ =>
    (1 : k)) (terminal.from ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk 0))).V)
    LinearMap.id fun i => rfl,
  LinearMap.id_comp]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (forget₂ (Rep k G) (ModuleCat k)).map (ε k G) = Finsupp.total (Fin 1 → G) k k fun x => 1
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ LinearMap.comp (Finsupp.total (⊤_ Type u) k k fun x => 1) ((ModuleCat.free k).map (terminal.from (Fin 1 → G))) =
    HomologicalComplex.Hom.f
        (SimplicialObject.Augmented.ExtraDegeneracy.homotopyEquiv (extraDegeneracyCompForgetAugmentedToModule k G)).hom
        0 ≫
      HomologicalComplex.Hom.f
        (HomotopyEquiv.ofIso
            ((ChainComplex.single₀ (ModuleCat k)).mapIso
              (LinearEquiv.toModuleIso (Finsupp.LinearEquiv.finsuppUnique k k (⊤_ Type u))))).hom
        0
[PROOFSTEP]
congr
[GOAL]
case e_f
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (Finsupp.total (⊤_ Type u) k k fun x => 1) =
    HomologicalComplex.Hom.f
      (HomotopyEquiv.ofIso
          ((ChainComplex.single₀ (ModuleCat k)).mapIso
            (LinearEquiv.toModuleIso (Finsupp.LinearEquiv.finsuppUnique k k (⊤_ Type u))))).hom
      0
[PROOFSTEP]
ext x
[GOAL]
case e_f.h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
x : ⊤_ Type u
⊢ ↑(LinearMap.comp (Finsupp.total (⊤_ Type u) k k fun x => 1) (Finsupp.lsingle x)) 1 =
    ↑(LinearMap.comp
          (HomologicalComplex.Hom.f
            (HomotopyEquiv.ofIso
                ((ChainComplex.single₀ (ModuleCat k)).mapIso
                  (LinearEquiv.toModuleIso (Finsupp.LinearEquiv.finsuppUnique k k (⊤_ Type u))))).hom
            0)
          (Finsupp.lsingle x))
      1
[PROOFSTEP]
dsimp [HomotopyEquiv.ofIso, Finsupp.LinearEquiv.finsuppUnique]
[GOAL]
case e_f.h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
x : ⊤_ Type u
⊢ ↑(Finsupp.total (⊤_ Type u) k k fun x => 1) (Finsupp.single x 1) = ↑(Finsupp.single x 1) default
[PROOFSTEP]
rw [Finsupp.total_single, one_smul, @Unique.eq_default _ Types.terminalIso.toEquiv.unique x, Finsupp.single_eq_same]
[GOAL]
case e_g.e_a
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ terminal.from (Fin 1 → G) = fun a => NatTrans.app (compForgetAugmented G).hom (Opposite.op (SimplexCategory.mk 0)) a
[PROOFSTEP]
exact @Subsingleton.elim _ (@Unique.instSubsingleton _ (Limits.uniqueToTerminal _)) _ _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ HomologicalComplex.d (resolution k G) 1 0 ≫ ε k G = 0
[PROOFSTEP]
ext : 1
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (HomologicalComplex.d (resolution k G) 1 0 ≫ ε k G).hom = 0.hom
[PROOFSTEP]
refine' LinearMap.ext fun x => _
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
x : ↑(HomologicalComplex.X (resolution k G) 1).V
⊢ ↑(HomologicalComplex.d (resolution k G) 1 0 ≫ ε k G).hom x = ↑0.hom x
[PROOFSTEP]
have : (forget₂ToModuleCat k G).d 1 0 ≫ (forget₂ (Rep k G) (ModuleCat.{u} k)).map (ε k G) = 0 :=
  by
  rw [← forget₂ToModuleCatHomotopyEquiv_f_0_eq, ← (forget₂ToModuleCatHomotopyEquiv k G).1.2 1 0 rfl]
  exact comp_zero
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
x : ↑(HomologicalComplex.X (resolution k G) 1).V
⊢ HomologicalComplex.d (forget₂ToModuleCat k G) 1 0 ≫ (forget₂ (Rep k G) (ModuleCat k)).map (ε k G) = 0
[PROOFSTEP]
rw [← forget₂ToModuleCatHomotopyEquiv_f_0_eq, ← (forget₂ToModuleCatHomotopyEquiv k G).1.2 1 0 rfl]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
x : ↑(HomologicalComplex.X (resolution k G) 1).V
⊢ HomologicalComplex.Hom.f (forget₂ToModuleCatHomotopyEquiv k G).hom 1 ≫
      HomologicalComplex.d
        ((ChainComplex.single₀ (ModuleCat k)).obj ((forget₂ (Rep k G) (ModuleCat k)).obj (Rep.trivial k G k))) 1 0 =
    0
[PROOFSTEP]
exact comp_zero
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
x : ↑(HomologicalComplex.X (resolution k G) 1).V
this : HomologicalComplex.d (forget₂ToModuleCat k G) 1 0 ≫ (forget₂ (Rep k G) (ModuleCat k)).map (ε k G) = 0
⊢ ↑(HomologicalComplex.d (resolution k G) 1 0 ≫ ε k G).hom x = ↑0.hom x
[PROOFSTEP]
exact LinearMap.ext_iff.1 this _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (Functor.mapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
      NatTrans.app (ChainComplex.single₀MapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k))).hom
        (Rep.trivial k G k) =
    (forget₂ToModuleCatHomotopyEquiv k G).hom
[PROOFSTEP]
refine' ChainComplex.to_single₀_ext _ _ _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ HomologicalComplex.Hom.f
      ((Functor.mapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
        NatTrans.app (ChainComplex.single₀MapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k))).hom
          (Rep.trivial k G k))
      0 =
    HomologicalComplex.Hom.f (forget₂ToModuleCatHomotopyEquiv k G).hom 0
[PROOFSTEP]
dsimp
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (forget₂ (Rep k G) (ModuleCat k)).map (HomologicalComplex.Hom.f (εToSingle₀ k G) 0) ≫
      𝟙 ((forget₂ (Rep k G) (ModuleCat k)).obj (Rep.trivial k G k)) =
    HomologicalComplex.Hom.f (forget₂ToModuleCatHomotopyEquiv k G).hom 0
[PROOFSTEP]
rw [Category.comp_id]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (forget₂ (Rep k G) (ModuleCat k)).map (HomologicalComplex.Hom.f (εToSingle₀ k G) 0) =
    HomologicalComplex.Hom.f (forget₂ToModuleCatHomotopyEquiv k G).hom 0
[PROOFSTEP]
exact (forget₂ToModuleCatHomotopyEquiv_f_0_eq k G).symm
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ QuasiIso
    ((Functor.mapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)).map (εToSingle₀ k G))
[PROOFSTEP]
have h : QuasiIso (forget₂ToModuleCatHomotopyEquiv k G).hom := HomotopyEquiv.toQuasiIso _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
h : QuasiIso (forget₂ToModuleCatHomotopyEquiv k G).hom
⊢ QuasiIso
    ((Functor.mapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)).map (εToSingle₀ k G))
[PROOFSTEP]
rw [← εToSingle₀_comp_eq k G] at h
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
h :
  QuasiIso
    ((Functor.mapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
      NatTrans.app (ChainComplex.single₀MapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k))).hom
        (Rep.trivial k G k))
⊢ QuasiIso
    ((Functor.mapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)).map (εToSingle₀ k G))
[PROOFSTEP]
haveI := h
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
h this :
  QuasiIso
    ((Functor.mapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
      NatTrans.app (ChainComplex.single₀MapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k))).hom
        (Rep.trivial k G k))
⊢ QuasiIso
    ((Functor.mapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)).map (εToSingle₀ k G))
[PROOFSTEP]
exact quasiIso_of_comp_right _ ((ChainComplex.single₀MapHomologicalComplex _).hom.app _)