-- Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
theorem actionDiagonalSucc_hom_apply {G : Type u} [Group G] {n : ℕ} (f : Fin (n + 1) → G) :
    (actionDiagonalSucc G n).hom.hom f = (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f i.succ)

Proof state:
G : Type u
inst✝ : Group G
n : ℕ
f : Fin (n + 1) → G
⊢ (actionDiagonalSucc G n).hom.hom f = (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)

Tactic:
induction n with
| zero => exact Prod.ext rfl (funext fun x => Fin.elim0 x)
| succ n hn =>
  refine Prod.ext rfl (funext fun x => ?_)
  
  dsimp [actionDiagonalSucc]
  erw [hn (fun (j : Fin (n + 1)) => f j.succ)]
  exact Fin.cases rfl (fun i => rfl) x

Result:
no goals

Proof state:
case succ
G : Type u
inst✝ : Group G
n : ℕ
hn : ∀ (f : Fin (n + 1) → G), (actionDiagonalSucc G n).hom.hom f = (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
x : Fin (n + 1)
⊢ (Fin.insertNthEquiv (fun x => G) 0)
      ((leftRegular G ⊗ { V := Fin n → G, ρ := 1 }).ρ ((Fin.consEquiv fun a => G).symm f).1⁻¹
        (f (Fin.succ 0), fun i => (f i.castSucc.succ)⁻¹ * f i.succ.succ))
      x =
    (f x.castSucc)⁻¹ * f x.succ

Tactic:
exact Fin.cases rfl (fun i => rfl) x

Result:
no goals

Proof state:
case zero
G : Type u
inst✝ : Group G
f : Fin (0 + 1) → G
⊢ (actionDiagonalSucc G 0).hom.hom f = (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)

Tactic:
exact Prod.ext rfl (funext fun x => Fin.elim0 x)

Result:
no goals

Proof state:
case succ
G : Type u
inst✝ : Group G
n : ℕ
hn : ∀ (f : Fin (n + 1) → G), (actionDiagonalSucc G n).hom.hom f = (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
x : Fin (n + 1)
⊢ (Fin.insertNthEquiv (fun x => G) 0)
      ((leftRegular G ⊗ { V := Fin n → G, ρ := 1 }).ρ ((Fin.consEquiv fun a => G).symm f).1⁻¹
        ((actionDiagonalSucc G n).hom.hom ((Fin.consEquiv fun a => G).symm f).2))
      x =
    (f x.castSucc)⁻¹ * f x.succ

Tactic:
erw [hn (fun (j : Fin (n + 1)) => f j.succ)]

Result:
case succ
G : Type u
inst✝ : Group G
n : ℕ
hn : ∀ (f : Fin (n + 1) → G), (actionDiagonalSucc G n).hom.hom f = (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
x : Fin (n + 1)
⊢ (Fin.insertNthEquiv (fun x => G) 0)
      ((leftRegular G ⊗ { V := Fin n → G, ρ := 1 }).ρ ((Fin.consEquiv fun a => G).symm f).1⁻¹
        (f (Fin.succ 0), fun i => (f i.castSucc.succ)⁻¹ * f i.succ.succ))
      x =
    (f x.castSucc)⁻¹ * f x.succ

Proof state:
case succ
G : Type u
inst✝ : Group G
n : ℕ
hn : ∀ (f : Fin (n + 1) → G), (actionDiagonalSucc G n).hom.hom f = (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
⊢ (actionDiagonalSucc G (n + 1)).hom.hom f = (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)

Tactic:
refine Prod.ext rfl (funext fun x => ?_)

Result:
case succ
G : Type u
inst✝ : Group G
n : ℕ
hn : ∀ (f : Fin (n + 1) → G), (actionDiagonalSucc G n).hom.hom f = (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
x : Fin (n + 1)
⊢ ((actionDiagonalSucc G (n + 1)).hom.hom f).2 x = (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ).2 x

Proof state:
case succ
G : Type u
inst✝ : Group G
n : ℕ
hn : ∀ (f : Fin (n + 1) → G), (actionDiagonalSucc G n).hom.hom f = (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
x : Fin (n + 1)
⊢ ((actionDiagonalSucc G (n + 1)).hom.hom f).2 x = (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ).2 x

Tactic:
dsimp [actionDiagonalSucc]

Result:
case succ
G : Type u
inst✝ : Group G
n : ℕ
hn : ∀ (f : Fin (n + 1) → G), (actionDiagonalSucc G n).hom.hom f = (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
x : Fin (n + 1)
⊢ (Fin.insertNthEquiv (fun x => G) 0)
      ((leftRegular G ⊗ { V := Fin n → G, ρ := 1 }).ρ ((Fin.consEquiv fun a => G).symm f).1⁻¹
        ((actionDiagonalSucc G n).hom.hom ((Fin.consEquiv fun a => G).symm f).2))
      x =
    (f x.castSucc)⁻¹ * f x.succ