awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
i : Fin (n + 1) → G
⊢ HSMul.hSMul (β := (i : Fin (n + 1)) → G) (i 0) (Fin.partialProd fun (i_1 : Fin n) ↦ i i_1.succ) =
    Fin.partialProd i ∘ Fin.succ

Tactic:
exact funext fun j ↦ Fin.partialProd_succ' i j |>.symm

Premises used: funext, Fin.partialProd_succ', Eq.symm
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
i : Fin (n + 1) → G
⊢ Eq (α := ((i : Fin (n + 1)) → G) →₀ k)
    (single (HSMul.hSMul (β := (i : Fin (n + 1)) → G) (i 0) (Fin.partialProd fun (i_1 : Fin n) ↦ i i_1.succ)) 1)
    (single (Fin.partialProd i ∘ Fin.succ) 1)

Tactic:
have eq3 : single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) (1 : k) =
      single (Fin.partialProd i ∘ Fin.succ) 1 := by
      congr; exact funext fun j ↦ Fin.partialProd_succ' i j |>.symm
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
i : Fin (n + 1) → G
eq3 :
  Eq (α := ((i : Fin (n + 1)) → G) →₀ k)
    (single (HSMul.hSMul (β := (i : Fin (n + 1)) → G) (i 0) (Fin.partialProd fun (i_1 : Fin n) ↦ i i_1.succ)) 1)
    (single (Fin.partialProd i ∘ Fin.succ) 1)
simp :
  HAdd.hAdd (α := (Fin (n + 1) → G) →₀ k)
      (single (HSMul.hSMul (β := (i : Fin (n + 1)) → G) (i 0) (Fin.partialProd fun (i_1 : Fin n) ↦ i i_1.succ)) 1)
      (∑ x : Fin (n + 1),
        single (Fin.partialProd (x.contractNth (fun (x1 x2 : G) ↦ x1 * x2) i))
          (HPow.hPow (α := k) (-1) ((↑x : ℕ) + 1))) =
    (standardComplex.d k G (n + 1) : (a : (Fin (n + 1 + 1) → G) →₀ k) → (Fin (n + 1) → G) →₀ k)
      (single (Fin.partialProd i) 1)
⊢ Eq (α := (↑(diagonal k G (n + 1)) : Type u))
    ((Hom.hom (d k G n ≫ Iso.inv (diagonalSuccIsoFree k G n)) :
          (a : (↑(free k G (Fin (n + 1) → G)) : Type u)) → (↑(diagonal k G (n + 1)) : Type u))
        (single i (single 1 1)) :
      (↑(diagonal k G (n + 1)) : Type u))
    ((Hom.hom (Iso.inv (diagonalSuccIsoFree k G (n + 1)) ≫ HomologicalComplex.d (standardComplex k G) (n + 1) n) :
          (a : (↑(free k G (Fin (n + 1) → G)) : Type u)) → (↑(diagonal k G (n + 1)) : Type u))
        (single i (single 1 1)) :
      (↑(diagonal k G (n + 1)) : Type u))

Tactic:
simp [μ_hom, d_single (k := k),
      Representation.linearizeOfMulActionIso_symm_apply,
      Representation.linearizeTrivialIso_symm_apply _, d_apply (k := k),
      Representation.μ_apply_single_single_leftRegular _,
      Representation.linearizeMap_single_diagonal _]

Premises used: Rep.μ_hom, _private.0.Representation.μ_apply_single_single_leftRegular, _private.0.Representation.linearizeMap_single_diagonal, Representation.linearizeOfMulActionIso_symm_apply, Rep.standardComplex.d_apply, Rep.barComplex.d_single, Representation.linearizeTrivialIso_symm_apply
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
i : Fin (n + 1) → G
eq3 :
  Eq (α := ((i : Fin (n + 1)) → G) →₀ k)
    (single (HSMul.hSMul (β := (i : Fin (n + 1)) → G) (i 0) (Fin.partialProd fun (i_1 : Fin n) ↦ i i_1.succ)) 1)
    (single (Fin.partialProd i ∘ Fin.succ) 1)
⊢ HAdd.hAdd (α := (Fin (n + 1) → G) →₀ k)
      (single (HSMul.hSMul (β := (i : Fin (n + 1)) → G) (i 0) (Fin.partialProd fun (i_1 : Fin n) ↦ i i_1.succ)) 1)
      (∑ x : Fin (n + 1),
        single (Fin.partialProd (x.contractNth (fun (x1 x2 : G) ↦ x1 * x2) i))
          (HPow.hPow (α := k) (-1) ((↑x : ℕ) + 1))) =
    (standardComplex.d k G (n + 1) : (a : (Fin (n + 1 + 1) → G) →₀ k) → (Fin (n + 1) → G) →₀ k)
      (single (Fin.partialProd i) 1)

Tactic:
simp [Fin.partialProd_contractNth, Fin.sum_univ_succ, Action.ofMulAction_V, eq3]

Premises used: Fin.partialProd_contractNth, Action.ofMulAction_V, Fin.sum_univ_succ
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
m : ℕ
rw :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (barComplex.d k G (m + 1) ≫ barComplex.d k G m ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
rw₁ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (barComplex.d k G (m + 1) ≫
      Iso.inv (diagonalSuccIsoFree k G (m + 1)) ≫ HomologicalComplex.d (standardComplex k G) (m + 1) m)
    0
rw₂ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ Iso.inv (diagonalSuccIsoFree k G (m + 1))) ≫
      HomologicalComplex.d (standardComplex k G) (m + 1) m)
    0
rw₃ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (CategoryStruct.comp (Y := diagonal k G (m + 1 + 1))
        (Iso.inv (diagonalSuccIsoFree k G (m + 1 + 1)) ≫ HomologicalComplex.d (standardComplex k G) (m + 1 + 1) (m + 1))
        (HomologicalComplex.d (standardComplex k G) (m + 1) m) :
      Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (0 : Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
rw₄ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (Iso.inv (diagonalSuccIsoFree k G (m + 1 + 1)) ≫
      CategoryStruct.comp (Y := diagonal k G (m + 1 + 1))
        (HomologicalComplex.d (standardComplex k G) (m + 1 + 1) (m + 1))
        (HomologicalComplex.d (standardComplex k G) (m + 1) m))
    0
rw₅ :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    (Iso.inv (diagonalSuccIsoFree k G (m + 1 + 1)) ≫ 0) 0
rw₆ rw₇ : Eq.{u + 1} (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1))) 0 0
⊢ Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0

Tactic:
rw [Category.assoc, d_comp_diagonalSuccIsoFree_inv_eq, ← Category.assoc,
        d_comp_diagonalSuccIsoFree_inv_eq, Category.assoc, HomologicalComplex.d_comp_d,
        Limits.comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, HomologicalComplex.d_comp_d, Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
m : ℕ
⊢ Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0

Tactic:
have key : (d k G (m + 1) ≫ d k G m) ≫ (diagonalSuccIsoFree k G m).inv = 0 := by
      rw [Category.assoc, d_comp_diagonalSuccIsoFree_inv_eq, ← Category.assoc,
        d_comp_diagonalSuccIsoFree_inv_eq, Category.assoc, HomologicalComplex.d_comp_d,
        Limits.comp_zero]
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
m : ℕ
key :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
⊢ Eq (α :=
    Quiver.Hom (V := Rep k G) ((fun (n : ℕ) ↦ (free k G (Fin n → G) : Rep k G)) (m + 1 + 1)) (diagonal k G (m + 1)))
    (CategoryStruct.comp (Y := (fun (n : ℕ) ↦ (free k G (Fin n → G) : Rep k G)) (m + 1))
        ((fun (n : ℕ) ↦
            (barComplex.d k G n : Quiver.Hom (V := Rep k G) (free k G (Fin (n + 1) → G)) (free k G (Fin n → G))))
          (m + 1))
        ((fun (n : ℕ) ↦
            (barComplex.d k G n : Quiver.Hom (V := Rep k G) (free k G (Fin (n + 1) → G)) (free k G (Fin n → G))))
          m) ≫
      Iso.inv (diagonalSuccIsoFree k G m))
    (0 ≫ Iso.inv (diagonalSuccIsoFree k G m))

Tactic:
simpa using key
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
m : ℕ
key :
  Eq (α := Quiver.Hom (V := Rep k G) (free k G (Fin (m + 1 + 1) → G)) (diagonal k G (m + 1)))
    ((barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ Iso.inv (diagonalSuccIsoFree k G m)) 0
⊢ Eq.{u + 1} (α :=
    Quiver.Hom (V := Rep k G) ((fun (n : ℕ) ↦ (free k G (Fin n → G) : Rep k G)) (m + 1 + 1))
      ((fun (n : ℕ) ↦ (free k G (Fin n → G) : Rep k G)) m))
    (CategoryStruct.comp (Y := (fun (n : ℕ) ↦ (free k G (Fin n → G) : Rep k G)) (m + 1))
      ((fun (n : ℕ) ↦
          (barComplex.d k G n : Quiver.Hom (V := Rep k G) (free k G (Fin (n + 1) → G)) (free k G (Fin n → G))))
        (m + 1))
      ((fun (n : ℕ) ↦
          (barComplex.d k G n : Quiver.Hom (V := Rep k G) (free k G (Fin (n + 1) → G)) (free k G (Fin n → G))))
        m))
    0

Tactic:
exact (cancel_mono (diagonalSuccIsoFree k G m).inv).mp (by simpa using key)

Premises used: CategoryTheory.cancel_mono, Iff.mp, Rep.diagonalSuccIsoFree, CategoryTheory.Iso.inv
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
⊢ Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (n + 1)) (HomologicalComplex.X (barComplex k G) n))
    (HomologicalComplex.d (barComplex k G) (n + 1) n) (d k G n)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
j : ℕ
rw :
  Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
      (HomologicalComplex.X (standardComplex k G) j))
    (CategoryStruct.comp (Y := HomologicalComplex.X (standardComplex k G) (j + 1))
      (Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          (j + 1)))
      (HomologicalComplex.d (standardComplex k G) (j + 1) j))
    (d k G j ≫
      Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          j))
rw₁ :
  Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
      (HomologicalComplex.X (standardComplex k G) j))
    (Iso.inv (diagonalSuccIsoFree k G (j + 1)) ≫ HomologicalComplex.d (standardComplex k G) (j + 1) j)
    (d k G j ≫
      Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          j))
rw₂ :
  Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
      (HomologicalComplex.X (standardComplex k G) j))
    (Iso.inv (diagonalSuccIsoFree k G (j + 1)) ≫ HomologicalComplex.d (standardComplex k G) (j + 1) j)
    (d k G j ≫ Iso.inv (diagonalSuccIsoFree k G j))
rw₃ rw₄ :
  Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
      (HomologicalComplex.X (standardComplex k G) j))
    (Iso.inv (diagonalSuccIsoFree k G (j + 1)) ≫ HomologicalComplex.d (standardComplex k G) (j + 1) j)
    (Iso.inv (diagonalSuccIsoFree k G (j + 1)) ≫ HomologicalComplex.d (standardComplex k G) (j + 1) j)
⊢ Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
      (HomologicalComplex.X (standardComplex k G) j))
    (CategoryStruct.comp (Y := HomologicalComplex.X (standardComplex k G) (j + 1))
      (Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          (j + 1)))
      (HomologicalComplex.d (standardComplex k G) (j + 1) j))
    (HomologicalComplex.d (barComplex k G) (j + 1) j ≫
      Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          j))

Tactic:
rw [d_def, Iso.symm_hom, Iso.symm_hom, d_comp_diagonalSuccIsoFree_inv_eq]

Premises used: Rep.barComplex.d_def, CategoryTheory.Iso.symm_hom, Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst_3 : AddCommGroup A
inst_4 : Module k A
ρ : Representation k G A
inst_5 : AddCommGroup B
inst_6 : Module k B
f g : IndV φ ρ →ₗ[k] B
hfg : ∀ (h : H), f ∘ₗ mk φ ρ h = g ∘ₗ mk φ ρ h
⊢ f = g

Tactic:
Coinvariants.hom_ext <| TensorProduct.ext <| Finsupp.lhom_ext' fun h =>
    LinearMap.ext_ring <| hfg h

Premises used: Finsupp.lhom_ext', Representation.Coinvariants.hom_ext, LinearMap.ext_ring, TensorProduct.ext
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst_3 : AddCommGroup A
inst_4 : Module k A
ρ : Representation k G A
inst_5 : AddCommGroup B
inst_6 : Module k B
τ : Representation k G B
h : H
x : G
a :
  ∀ (a : H) (x_1 : A),
    Eq (α := TensorProduct k (H →₀ k) A)
      ((((TensorProduct.AlgebraTensorModule.curry
                      (LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * h⁻¹) ∘ₗ
                        (tprod (MonoidHom.comp (leftRegular k H) φ) ρ :
                            (a : G) → TensorProduct k (H →₀ k) A →ₗ[k] TensorProduct k (H →₀ k) A)
                          x) ∘ₗ
                    lsingle a :
                  k →ₗ[k] A →ₗ[k] TensorProduct k (H →₀ k) A) :
                (a : k) → A →ₗ[k] TensorProduct k (H →₀ k) A)
              1 :
            (a : A) → TensorProduct k (H →₀ k) A)
          x_1 :
        TensorProduct k (H →₀ k) A)
      ((((TensorProduct.AlgebraTensorModule.curry
                      ((tprod (MonoidHom.comp (leftRegular k H) φ) ρ :
                            (a : G) → TensorProduct k (H →₀ k) A →ₗ[k] TensorProduct k (H →₀ k) A)
                          x ∘ₗ
                        LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * h⁻¹)) ∘ₗ
                    lsingle a :
                  k →ₗ[k] A →ₗ[k] TensorProduct k (H →₀ k) A) :
                (a : k) → A →ₗ[k] TensorProduct k (H →₀ k) A)
              1 :
            (a : A) → TensorProduct k (H →₀ k) A)
          x_1 :
        TensorProduct k (H →₀ k) A)
⊢ Eq (α := TensorProduct k (H →₀ k) A →ₗ[k] TensorProduct k (H →₀ k) A)
    (LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * h⁻¹) ∘ₗ
      (tprod (MonoidHom.comp (leftRegular k H) φ) ρ :
          (a : G) → TensorProduct k (H →₀ k) A →ₗ[k] TensorProduct k (H →₀ k) A)
        x)
    ((tprod (MonoidHom.comp (leftRegular k H) φ) ρ :
          (a : G) → TensorProduct k (H →₀ k) A →ₗ[k] TensorProduct k (H →₀ k) A)
        x ∘ₗ
      LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * h⁻¹))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst_3 : AddCommGroup A
inst_4 : Module k A
ρ : Representation k G A
inst_5 : AddCommGroup B
inst_6 : Module k B
τ : Representation k G B
h : H
x : G
a : H
x_1 : A
⊢ Eq (α := TensorProduct k (H →₀ k) A)
    ((((TensorProduct.AlgebraTensorModule.curry
                    (LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * h⁻¹) ∘ₗ
                      (tprod (MonoidHom.comp (leftRegular k H) φ) ρ :
                          (a : G) → TensorProduct k (H →₀ k) A →ₗ[k] TensorProduct k (H →₀ k) A)
                        x) ∘ₗ
                  lsingle a :
                k →ₗ[k] A →ₗ[k] TensorProduct k (H →₀ k) A) :
              (a : k) → A →ₗ[k] TensorProduct k (H →₀ k) A)
            1 :
          (a : A) → TensorProduct k (H →₀ k) A)
        x_1 :
      TensorProduct k (H →₀ k) A)
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((tprod (MonoidHom.comp (leftRegular k H) φ) ρ :
                          (a : G) → TensorProduct k (H →₀ k) A →ₗ[k] TensorProduct k (H →₀ k) A)
                        x ∘ₗ
                      LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * h⁻¹)) ∘ₗ
                  lsingle a :
                k →ₗ[k] A →ₗ[k] TensorProduct k (H →₀ k) A) :
              (a : k) → A →ₗ[k] TensorProduct k (H →₀ k) A)
            1 :
          (a : A) → TensorProduct k (H →₀ k) A)
        x_1 :
      TensorProduct k (H →₀ k) A)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst_3 : AddCommGroup A
inst_4 : Module k A
ρ : Representation k G A
inst_5 : AddCommGroup B
inst_6 : Module k B
τ : Representation k G B
H₁ :
  ∀ (a : H) (x : A),
    Eq (α :=
      (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants (k := k) (G := G) (V := TensorProduct k (H →₀ k) A))
      ((((TensorProduct.AlgebraTensorModule.curry
                      (Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                          (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                          { toLinearMap := LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * 1⁻¹),
                            isIntertwining' := ⋯ } ∘ₗ
                        Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
                    lsingle a :
                  k →ₗ[k]
                    A →ₗ[k]
                      (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants (k := k) (G := G) (V :=
                        TensorProduct k (H →₀ k) A)) :
                (a : k) → A →ₗ[k] (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants)
              1 :
            (a : A) → (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants)
          x :
        (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants (k := k) (G := G) (V := TensorProduct k (H →₀ k) A))
      ((((TensorProduct.AlgebraTensorModule.curry
                      (1 ∘ₗ Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
                    lsingle a :
                  k →ₗ[k]
                    A →ₗ[k]
                      (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants (k := k) (G := G) (V :=
                        TensorProduct k (H →₀ k) A)) :
                (a : k) → A →ₗ[k] (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants)
              1 :
            (a : A) → (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants)
          x :
        (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants (k := k) (G := G) (V := TensorProduct k (H →₀ k) A))
⊢ Eq (α := IndV φ ρ →ₗ[k] IndV φ ρ)
    (Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
      { toLinearMap := LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * 1⁻¹), isIntertwining' := ⋯ })
    1

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst_3 : AddCommGroup A
inst_4 : Module k A
ρ : Representation k G A
inst_5 : AddCommGroup B
inst_6 : Module k B
τ : Representation k G B
a : H
x : A
⊢ Eq (α :=
    (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants (k := k) (G := G) (V := TensorProduct k (H →₀ k) A))
    ((((TensorProduct.AlgebraTensorModule.curry
                    (Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                        (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                        { toLinearMap := LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * 1⁻¹),
                          isIntertwining' := ⋯ } ∘ₗ
                      Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
                  lsingle a :
                k →ₗ[k]
                  A →ₗ[k]
                    (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants (k := k) (G := G) (V :=
                      TensorProduct k (H →₀ k) A)) :
              (a : k) → A →ₗ[k] (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants)
            1 :
          (a : A) → (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants)
        x :
      (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants (k := k) (G := G) (V := TensorProduct k (H →₀ k) A))
    ((((TensorProduct.AlgebraTensorModule.curry (1 ∘ₗ Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
                  lsingle a :
                k →ₗ[k]
                  A →ₗ[k]
                    (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants (k := k) (G := G) (V :=
                      TensorProduct k (H →₀ k) A)) :
              (a : k) → A →ₗ[k] (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants)
            1 :
          (a : A) → (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants)
        x :
      (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants (k := k) (G := G) (V := TensorProduct k (H →₀ k) A))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst_3 : AddCommGroup A
inst_4 : Module k A
ρ : Representation k G A
inst_5 : AddCommGroup B
inst_6 : Module k B
τ : Representation k G B
x x_1 : H
H₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
      { toLinearMap := LinearMap.rTensor A (lmapDomain k k fun (x_2 : H) ↦ x_2 * (x * x_1)⁻¹), isIntertwining' := ⋯ } =
    HMul.hMul (α := IndV φ ρ →ₗ[k] IndV φ ρ)
      (Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
        { toLinearMap := LinearMap.rTensor A (lmapDomain k k fun (x_2 : H) ↦ x_2 * x⁻¹), isIntertwining' := ⋯ :
          (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).IntertwiningMap
            (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) })
      (Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
        { toLinearMap := LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * x_1⁻¹), isIntertwining' := ⋯ :
          (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).IntertwiningMap
            (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) })

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst_3 : AddCommGroup A
inst_4 : Module k A
ρ : Representation k G A
inst_5 : AddCommGroup B
inst_6 : Module k B
τ : Representation k G B
x x_1 a : H
x_2 : A
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [IndV, mul_assoc]

Premises used: mul_assoc, Representation.IndV
-- Module: Mathlib.RepresentationTheory.Induced
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A : Type u_4
inst_3 : AddCommGroup A
inst_4 : Module k A
ρ : Representation k G A
h₁ h₂ : H
a : A
⊢ Eq (α := IndV φ ρ)
    ((((ind φ ρ : (a : H) → IndV φ ρ →ₗ[k] IndV φ ρ) h₁ : IndV φ ρ →ₗ[k] IndV φ ρ) : (a : IndV φ ρ) → IndV φ ρ)
        ((IndV.mk φ ρ h₂ : (a : A) → IndV φ ρ) a) :
      IndV φ ρ)
    ((IndV.mk φ ρ (h₂ * h₁⁻¹) : (a : A) → IndV φ ρ) a : IndV φ ρ)

Tactic:
simp