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

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

Tactic:
intro a b x _ _ hx

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

Tactic:
simp only [TensorProduct.zero_tmul, map_zero]

Result:
no goals

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

Tactic:
simp only [lift_apply, smul_single', map_add, hx, (diagonalSucc_inv_single_single),
  TensorProduct.add_tmul, Finsupp.sum_single_index, zero_mul, single_zero]

Result:
no goals

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

Tactic:
refine g.induction ?_ ?_

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

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