-- Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
theorem diagonalSucc_inv_single_left (g : G) (f : Gⁿ →₀ k) (r : k) :
    (diagonalSucc k G n).inv.hom (Finsupp.single g r ⊗ₜ f) =
      Finsupp.lift (Gⁿ⁺¹ →₀ k) k Gⁿ (fun f => single (g • partialProd f) r) f

Proof state:
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
x : (Fin n → G) →₀ k
a✝¹ : a ∉ x.support
a✝ : b ≠ 0
hx :
  (ConcreteCategory.hom (diagonalSucc k G n).inv.hom) (single g r ⊗ₜ[k] x) =
    ((lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) x
⊢ (ConcreteCategory.hom (diagonalSucc k G n).inv.hom) (single g r ⊗ₜ[k] (single a b + x)) =
    ((lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) (single a b + x)

Tactic:
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]

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : (Fin n → G) →₀ k
r : k
⊢ (ConcreteCategory.hom (diagonalSucc k G n).inv.hom) (single g r ⊗ₜ[k] f) =
    ((lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) f

Tactic:
refine f.induction ?_ ?_

Result:
case refine_1
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : (Fin n → G) →₀ k
r : k
⊢ (ConcreteCategory.hom (diagonalSucc k G n).inv.hom) (single g r ⊗ₜ[k] 0) =
    ((lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) 0

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 →
        (ConcreteCategory.hom (diagonalSucc k G n).inv.hom) (single g r ⊗ₜ[k] f) =
            ((lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) f →
          (ConcreteCategory.hom (diagonalSucc k G n).inv.hom) (single g r ⊗ₜ[k] (single a b + f)) =
            ((lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) (single a b + f)

Proof state:
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 →
        (ConcreteCategory.hom (diagonalSucc k G n).inv.hom) (single g r ⊗ₜ[k] f) =
            ((lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) f →
          (ConcreteCategory.hom (diagonalSucc k G n).inv.hom) (single g r ⊗ₜ[k] (single a b + f)) =
            ((lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) (single a b + f)

Tactic:
intro a b x _ _ hx

Result:
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
x : (Fin n → G) →₀ k
a✝¹ : a ∉ x.support
a✝ : b ≠ 0
hx :
  (ConcreteCategory.hom (diagonalSucc k G n).inv.hom) (single g r ⊗ₜ[k] x) =
    ((lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) x
⊢ (ConcreteCategory.hom (diagonalSucc k G n).inv.hom) (single g r ⊗ₜ[k] (single a b + x)) =
    ((lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) (single a b + x)

Proof state:
case refine_1
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : (Fin n → G) →₀ k
r : k
⊢ (ConcreteCategory.hom (diagonalSucc k G n).inv.hom) (single g r ⊗ₜ[k] 0) =
    ((lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) 0

Tactic:
simp only [TensorProduct.tmul_zero, map_zero]

Result:
no goals