Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: case succ.zero
G : Type u
inst✝ : Group G
n : ℕ
f : Fin (n + 1 + 1) → G
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
⊢ (Fin.consEquiv fun x ↦ G)
      ({ toFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1)) g.2),
            left_inv := ⋯, right_inv := ⋯ }
          (((Fin.consEquiv fun a ↦ G).symm f).1, ((Fin.consEquiv fun a ↦ G).symm f).2 0, fun i ↦
            (((Fin.consEquiv fun a ↦ G).symm f).2 i.castSucc)⁻¹ * ((Fin.consEquiv fun a ↦ G).symm f).2 i.succ)).2
      0 =
    (f 0)⁻¹ * f 1

pp: case succ.succ
G : Type u
inst✝ : Group G
n : ℕ
f : Fin (n + 1 + 1) → G
i✝ : Fin n
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
⊢ (Fin.consEquiv fun x ↦ G)
      ({ toFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1)) g.2),
            left_inv := ⋯, right_inv := ⋯ }
          (((Fin.consEquiv fun a ↦ G).symm f).1, ((Fin.consEquiv fun a ↦ G).symm f).2 0, fun i ↦
            (((Fin.consEquiv fun a ↦ G).symm f).2 i.castSucc)⁻¹ * ((Fin.consEquiv fun a ↦ G).symm f).2 i.succ)).2
      i✝.succ =
    (f i✝.castSucc.succ)⁻¹ * f i✝.succ.succ

Tactic:
<;>

Goal state after:
case succ.zero
G : Type u
inst✝ : Group G
n : ℕ
f : Fin (n + 1 + 1) → G
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
⊢ (Fin.consEquiv fun x ↦ G)
      ({ toFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1)) g.2),
            left_inv := ⋯, right_inv := ⋯ }
          (((Fin.consEquiv fun a ↦ G).symm f).1, ((Fin.consEquiv fun a ↦ G).symm f).2 0, fun i ↦
            (((Fin.consEquiv fun a ↦ G).symm f).2 i.castSucc)⁻¹ * ((Fin.consEquiv fun a ↦ G).symm f).2 i.succ)).2
      0 =
    (f 0)⁻¹ * f 1

case succ.succ
G : Type u
inst✝ : Group G
n : ℕ
f : Fin (n + 1 + 1) → G
i✝ : Fin n
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
⊢ (Fin.consEquiv fun x ↦ G)
      ({ toFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1)) g.2),
            left_inv := ⋯, right_inv := ⋯ }
          (((Fin.consEquiv fun a ↦ G).symm f).1, ((Fin.consEquiv fun a ↦ G).symm f).2 0, fun i ↦
            (((Fin.consEquiv fun a ↦ G).symm f).2 i.castSucc)⁻¹ * ((Fin.consEquiv fun a ↦ G).symm f).2 i.succ)).2
      i✝.succ =
    (f i✝.castSucc.succ)⁻¹ * f i✝.succ.succ