awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
y : asModule (V := G →₀ k) (ofMulAction k G G)
g a : G
⊢ Eq.{u_1 + 1} (α := k)
    ((((((asAlgebraHom (ofMulAction k G G) : (a : k[G]) → End k (G →₀ k)) ((of k G : (a : G) → k[G]) g) :
                  End k (G →₀ k)) :
                (a : G →₀ k) → G →₀ k)
              y :
            G →₀ k) :
          (a : G) → k)
        a :
      k)
    ((HMul.hMul (α := k[G]) ((of k G : (a : G) → k[G]) g : k[G]) y : (a : G) → k) a : k)

Tactic:
simp [(MonoidAlgebra.single_mul_apply)]

Premises used: MonoidAlgebra.single_mul_apply
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
y_1 : asModule (V := G →₀ k) (ofMulAction k G G)
x y : k[G]
hx : x • y_1 = x * y_1
hy : y • y_1 = y * y_1
⊢ (x + y) • y_1 = (x + y) * y_1

Tactic:
simp only [hx, hy, add_mul, add_smul]

Premises used: add_mul, add_smul
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
y : asModule (V := G →₀ k) (ofMulAction k G G)
r : k
x : k[G]
hx : x • y = x * y
⊢ (r • x) • y = r • x * y

Tactic:
simp [← hx]
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
x : k[G]
y : asModule (V := G →₀ k) (ofMulAction k G G)
hM :
  ∀ (g : G),
    HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) g : k[G]) y =
      HMul.hMul (α := k[G]) ((of k G : (a : G) → k[G]) g : k[G]) y
hadd : ∀ (x y_1 : k[G]) (hx : x • y = x * y) (hy : y_1 • y = y_1 * y), (x + y_1) • y = (x + y_1) * y
hsmul : ∀ (r : k) (x : k[G]) (hx : x • y = x * y), (r • x) • y = r • x * y
⊢ x • y = x * y

Tactic:
induction x using MonoidAlgebra.induction_on with
  | hM g =>
    change asAlgebraHom (ofMulAction k G G) _ _ = _
    ext
    -- Porting note: single_mul_apply not firing in simp without parentheses, probably due to the
    -- defeq abuse in `change` above.
    simp [(MonoidAlgebra.single_mul_apply)]
  | hadd x y hx hy => simp only [hx, hy, add_mul, add_smul]
  | hsmul r x hx => simp [← hx]

Premises used: add_mul, Representation.asAlgebraHom, MonoidAlgebra.single_mul_apply, Representation.ofMulAction, add_smul, MonoidAlgebra.induction_on, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
g : G
⊢ Eq.{u_3 + 1} (α := V →ₗ[k] V) ((↑((ρ.asGroupHom : (a : G) → (V →ₗ[k] V)ˣ) g) : V →ₗ[k] V) : V →ₗ[k] V)
    ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V)

Tactic:
simp only [asGroupHom, MonoidHom.coe_toHomUnits]

Premises used: MonoidHom.coe_toHomUnits, Representation.asGroupHom
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
h :
  ∀ (i : G),
    Eq (α := G →₀ k) ((norm (leftRegular k G) ∘ₗ lsingle i : (a : k) → G →₀ k) 1)
      ((((LinearMap.flip (lsmul k (G →₀ k)) : (a : G →₀ k) → k →ₗ[k] G →₀ k)
                ((norm (leftRegular k G) : (a : G →₀ k) → G →₀ k) (Finsupp.single 1 1)) ∘ₗ
              linearCombination k fun (x : G) ↦ 1) ∘ₗ
            lsingle i :
          (a : k) → G →₀ k)
        1)
⊢ norm (leftRegular k G) =
    (LinearMap.flip (lsmul k (G →₀ k)) : (a : G →₀ k) → k →ₗ[k] G →₀ k)
        ((norm (leftRegular k G) : (a : G →₀ k) → G →₀ k) (Finsupp.single 1 1)) ∘ₗ
      linearCombination k fun (x : G) ↦ 1

Tactic:
ext i : 2
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
i : G
⊢ ∀ (i_1 : G), Membership.mem (γ := Finset G) Finset.univ i_1 ↔ Membership.mem (γ := Finset G) Finset.univ (i_1 * i)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
i : G
⊢ ∀ (i_1 : G),
    Membership.mem (γ := Finset G) Finset.univ i_1 →
      Eq (α := G →₀ k) (Finsupp.single (i_1 * i) 1) (Finsupp.single (i_1 * i) 1)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
i : G
⊢ Eq (α := G →₀ k) ((norm (leftRegular k G) ∘ₗ lsingle i : (a : k) → G →₀ k) 1)
    ((((LinearMap.flip (lsmul k (G →₀ k)) : (a : G →₀ k) → k →ₗ[k] G →₀ k)
              ((norm (leftRegular k G) : (a : G →₀ k) → G →₀ k) (Finsupp.single 1 1)) ∘ₗ
            linearCombination k fun (x : G) ↦ 1) ∘ₗ
          lsingle i :
        (a : k) → G →₀ k)
      1)

Tactic:
simpa [Representation.norm] using Finset.sum_bijective _
    (Group.mulRight_bijective i) (by simp) (by simp)

Premises used: Group.mulRight_bijective, Finset.sum_bijective, Representation.norm
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
x : G →₀ k
rw :
  Eq (α := G →₀ k)
      (((LinearMap.flip (lsmul k (G →₀ k)) : (a : G →₀ k) → k →ₗ[k] G →₀ k)
                ((norm (leftRegular k G) : (a : G →₀ k) → G →₀ k) (Finsupp.single 1 1)) ∘ₗ
              linearCombination k fun (x : G) ↦ 1 :
            (a : G →₀ k) → G →₀ k)
          x :
        G →₀ k)
      (0 : G →₀ k) ↔
    Eq.{u_1 + 1} (α := k) ((linearCombination k fun (x : G) ↦ 1 : (a : G →₀ k) → k) x : k) (0 : k)
⊢ Eq (α := G →₀ k) ((norm (leftRegular k G) : (a : G →₀ k) → G →₀ k) x : G →₀ k) (0 : G →₀ k) ↔
    Eq.{u_1 + 1} (α := k) ((linearCombination k fun (x : G) ↦ 1 : (a : G →₀ k) → k) x : k) (0 : k)

Tactic:
rw [leftRegular_norm_apply]

Premises used: Representation.leftRegular_norm_apply
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
x : G →₀ k
mp :
  Eq (α := G →₀ k)
      (((LinearMap.flip (lsmul k (G →₀ k)) : (a : G →₀ k) → k →ₗ[k] G →₀ k)
                ((norm (leftRegular k G) : (a : G →₀ k) → G →₀ k) (Finsupp.single 1 1)) ∘ₗ
              linearCombination k fun (x : G) ↦ 1 :
            (a : G →₀ k) → G →₀ k)
          x :
        G →₀ k)
      (0 : G →₀ k) →
    Eq.{u_1 + 1} (α := k) ((linearCombination k fun (x : G) ↦ 1 : (a : G →₀ k) → k) x : k) (0 : k)
mpr :
  Eq.{u_1 + 1} (α := k) ((linearCombination k fun (x : G) ↦ 1 : (a : G →₀ k) → k) x : k) (0 : k) →
    Eq (α := G →₀ k)
      (((LinearMap.flip (lsmul k (G →₀ k)) : (a : G →₀ k) → k →ₗ[k] G →₀ k)
                ((norm (leftRegular k G) : (a : G →₀ k) → G →₀ k) (Finsupp.single 1 1)) ∘ₗ
              linearCombination k fun (x : G) ↦ 1 :
            (a : G →₀ k) → G →₀ k)
          x :
        G →₀ k)
      (0 : G →₀ k)
⊢ Eq (α := G →₀ k)
      (((LinearMap.flip (lsmul k (G →₀ k)) : (a : G →₀ k) → k →ₗ[k] G →₀ k)
                ((norm (leftRegular k G) : (a : G →₀ k) → G →₀ k) (Finsupp.single 1 1)) ∘ₗ
              linearCombination k fun (x : G) ↦ 1 :
            (a : G →₀ k) → G →₀ k)
          x :
        G →₀ k)
      (0 : G →₀ k) ↔
    Eq.{u_1 + 1} (α := k) ((linearCombination k fun (x : G) ↦ 1 : (a : G →₀ k) → k) x : k) (0 : k)

Tactic:
constructor
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
x : G →₀ k
h :
  Eq (α := G →₀ k)
    (((LinearMap.flip (lsmul k (G →₀ k)) : (a : G →₀ k) → k →ₗ[k] G →₀ k)
              ((norm (leftRegular k G) : (a : G →₀ k) → G →₀ k) (Finsupp.single 1 1)) ∘ₗ
            linearCombination k fun (x : G) ↦ 1 :
          (a : G →₀ k) → G →₀ k)
        x :
      G →₀ k)
    (0 : G →₀ k)
⊢ Eq.{u_1 + 1} (α := k) ((linearCombination k fun (x : G) ↦ 1 : (a : G →₀ k) → k) x : k) (0 : k)

Tactic:
simpa [norm, Representation.norm] using Finsupp.ext_iff.1 h 1

Premises used: Iff.mp, Representation.norm, OfNat.ofNat, Finsupp.ext_iff
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
x : G →₀ k
h : Eq.{u_1 + 1} (α := k) ((linearCombination k fun (x : G) ↦ 1 : (a : G →₀ k) → k) x : k) (0 : k)
mpr :
  ∀ (a : G),
    Eq.{u_1 + 1} (α := k)
      (((((LinearMap.flip (lsmul k (G →₀ k)) : (a : G →₀ k) → k →ₗ[k] G →₀ k)
                      ((norm (leftRegular k G) : (a : G →₀ k) → G →₀ k) (Finsupp.single 1 1)) ∘ₗ
                    linearCombination k fun (x : G) ↦ 1 :
                  (a : G →₀ k) → G →₀ k)
                x :
              G →₀ k) :
            (a : G) → k)
          a :
        k)
      ((0 : (a : G) → k) a : k)
⊢ Eq (α := G →₀ k)
    (((LinearMap.flip (lsmul k (G →₀ k)) : (a : G →₀ k) → k →ₗ[k] G →₀ k)
              ((norm (leftRegular k G) : (a : G →₀ k) → G →₀ k) (Finsupp.single 1 1)) ∘ₗ
            linearCombination k fun (x : G) ↦ 1 :
          (a : G →₀ k) → G →₀ k)
        x :
      G →₀ k)
    (0 : G →₀ k)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
x : G →₀ k
h : Eq.{u_1 + 1} (α := k) ((linearCombination k fun (x : G) ↦ 1 : (a : G →₀ k) → k) x : k) (0 : k)
a : G
⊢ Eq.{u_1 + 1} (α := k)
    (((((LinearMap.flip (lsmul k (G →₀ k)) : (a : G →₀ k) → k →ₗ[k] G →₀ k)
                    ((norm (leftRegular k G) : (a : G →₀ k) → G →₀ k) (Finsupp.single 1 1)) ∘ₗ
                  linearCombination k fun (x : G) ↦ 1 :
                (a : G →₀ k) → G →₀ k)
              x :
            G →₀ k) :
          (a : G) → k)
        a :
      k)
    ((0 : (a : G) → k) a : k)

Tactic:
simp_all
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
h :
  ∀ (x : G →₀ k),
    Membership.mem (γ := Submodule k (G →₀ k)) (ker (norm (leftRegular k G))) x ↔
      Membership.mem (γ := Submodule k (G →₀ k)) (ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x
⊢ Eq (α := Submodule k (G →₀ k)) (ker (norm (leftRegular k G))) (ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
x : G →₀ k
⊢ Membership.mem (γ := Submodule k (G →₀ k)) (ker (norm (leftRegular k G))) x ↔
    Membership.mem (γ := Submodule k (G →₀ k)) (ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x

Tactic:
leftRegular_norm_eq_zero_iff _

Premises used: Set.Mem, Representation.leftRegular_norm_eq_zero_iff, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
x : G →₀ k
⊢ Membership.mem (γ := Submodule k (G →₀ k)) (ker (norm (leftRegular k G))) x ↔
    Membership.mem (γ := Submodule k (G →₀ k)) (ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x

Tactic:
exact leftRegular_norm_eq_zero_iff _

Premises used: Representation.leftRegular_norm_eq_zero_iff
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : G →₀ k
hx : (((leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g : (G →₀ k) →ₗ[k] G →₀ k) : (a : G →₀ k) → G →₀ k) x = x
γ : G
rcases : ∀ (i : ℤ), Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) i) : k) ((x : (a : G) → k) g : k)
⊢ Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) γ : k) ((x : (a : G) → k) g : k)

Tactic:
rcases hg γ with ⟨i, rfl⟩

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : G →₀ k
hx : (((leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g : (G →₀ k) →ₗ[k] G →₀ k) : (a : G →₀ k) → G →₀ k) x = x
⊢ Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) 0) : k) ((x : (a : G) → k) g : k)

Tactic:
simpa using (Finsupp.ext_iff.1 hx g)

Premises used: Iff.mp, Finsupp.ext_iff
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : G →₀ k
hx : (((leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g : (G →₀ k) →ₗ[k] G →₀ k) : (a : G →₀ k) → G →₀ k) x = x
n : ℕ
h : Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) (↑n : ℤ)) : k) ((x : (a : G) → k) g : k)
⊢ Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) : k)
    ((x : (a : G) → k) g : k)

Tactic:
simpa [← h, zpow_natCast, zpow_add_one, pow_mul_comm', pow_succ'] using
      (Finsupp.ext_iff.1 hx (g ^ (n + 1))).symm

Premises used: zpow_natCast, zpow_add_one, pow_mul_comm', HPow.hPow, HAdd.hAdd, Iff.mp, OfNat.ofNat, Eq.symm, Finsupp.ext_iff, pow_succ'
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : G →₀ k
hx : (((leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g : (G →₀ k) →ₗ[k] G →₀ k) : (a : G →₀ k) → G →₀ k) x = x
n : ℕ
h : Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) (-(↑n : ℤ))) : k) ((x : (a : G) → k) g : k)
⊢ Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) : k)
    ((x : (a : G) → k) g : k)

Tactic:
simpa [zpow_sub, ← h, ← mul_inv_rev, ← pow_mul_comm']
      using Finsupp.ext_iff.1 hx (g ^ (-n : ℤ))

Premises used: Nat.cast, pow_mul_comm', HPow.hPow, Iff.mp, mul_inv_rev, Finsupp.ext_iff, Neg.neg, zpow_sub
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : G →₀ k
hx : (((leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g : (G →₀ k) →ₗ[k] G →₀ k) : (a : G →₀ k) → G →₀ k) x = x
i : ℤ
zero : Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) 0) : k) ((x : (a : G) → k) g : k)
succ :
  ∀ (n : ℕ)
    (h : Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) (↑n : ℤ)) : k) ((x : (a : G) → k) g : k)),
    Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) : k)
      ((x : (a : G) → k) g : k)
pred :
  ∀ (n : ℕ)
    (h : Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) (-(↑n : ℤ))) : k) ((x : (a : G) → k) g : k)),
    Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) : k)
      ((x : (a : G) → k) g : k)
⊢ Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) i) : k) ((x : (a : G) → k) g : k)

Tactic:
induction i with
  | zero =>
    simpa using (Finsupp.ext_iff.1 hx g)
  | succ n h =>
    simpa [← h, zpow_natCast, zpow_add_one, pow_mul_comm', pow_succ'] using
      (Finsupp.ext_iff.1 hx (g ^ (n + 1))).symm
  | pred n h =>
    simpa [zpow_sub, ← h, ← mul_inv_rev, ← pow_mul_comm']
      using Finsupp.ext_iff.1 hx (g ^ (-n : ℤ))

Premises used: zpow_natCast, zpow_add_one, pow_mul_comm', Iff.mp, mul_inv_rev, Finsupp.ext_iff, pow_succ', zpow_sub
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
ι : Type u_3
V : ι → Type u_4
inst_2 : (i : ι) → AddCommMonoid (V i)
inst_3 : (i : ι) → Module.{u_1, u_4} k (V i)
ρ : (i : ι) → Representation.{u_1, u_2, u_4} k G (V i)
h :
  ∀ (x : ⨁ (i : ι), V i) (i : ι),
    (((lmap (M := V) (N := V) fun (x : ι) ↦ (ρ x : (a : G) → V x →ₗ[k] V x) 1 : (a : ⨁ (i : ι), V i) → ⨁ (i : ι), V i)
              x :
            ⨁ (i : ι), V i) :
          (a : ι) → V a)
        i =
      (((1 : (a : ⨁ (i : ι), V i) → ⨁ (i : ι), V i) x : ⨁ (i : ι), V i) : (a : ι) → V a) i
⊢ Eq (α := (⨁ (i : ι), V i) →ₗ[k] ⨁ (i : ι), V i)
    (lmap (M := V) (N := V) fun (x : ι) ↦ (ρ x : (a : G) → V x →ₗ[k] V x) 1) 1

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
ι : Type u_3
V : ι → Type u_4
inst_2 : (i : ι) → AddCommMonoid (V i)
inst_3 : (i : ι) → Module.{u_1, u_4} k (V i)
ρ : (i : ι) → Representation.{u_1, u_2, u_4} k G (V i)
x : ⨁ (i : ι), V i
i : ι
⊢ (((lmap (M := V) (N := V) fun (x : ι) ↦ (ρ x : (a : G) → V x →ₗ[k] V x) 1 : (a : ⨁ (i : ι), V i) → ⨁ (i : ι), V i) x :
          ⨁ (i : ι), V i) :
        (a : ι) → V a)
      i =
    (((1 : (a : ⨁ (i : ι), V i) → ⨁ (i : ι), V i) x : ⨁ (i : ι), V i) : (a : ι) → V a) i

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
ι : Type u_3
V : ι → Type u_4
inst_2 : (i : ι) → AddCommMonoid (V i)
inst_3 : (i : ι) → Module.{u_1, u_4} k (V i)
ρ : (i : ι) → Representation.{u_1, u_2, u_4} k G (V i)
g h : G
h₁ :
  ∀ (x : ⨁ (i : ι), V i) (i : ι),
    (((lmap (M := V) (N := V) fun (x : ι) ↦ (ρ x : (a : G) → V x →ₗ[k] V x) (g * h) :
                (a : ⨁ (i : ι), V i) → ⨁ (i : ι), V i)
              x :
            ⨁ (i : ι), V i) :
          (a : ι) → V a)
        i =
      (((HMul.hMul (α := (⨁ (i : ι), V i) →ₗ[k] ⨁ (i : ι), V i)
                  (lmap (M := V) (N := V) fun (x : ι) ↦ (ρ x : (a : G) → V x →ₗ[k] V x) g)
                  (lmap (M := V) (N := V) fun (x : ι) ↦ (ρ x : (a : G) → V x →ₗ[k] V x) h) :
                (a : ⨁ (i : ι), V i) → ⨁ (i : ι), V i)
              x :
            ⨁ (i : ι), V i) :
          (a : ι) → V a)
        i
⊢ (lmap (M := V) (N := V) fun (x : ι) ↦ (ρ x : (a : G) → V x →ₗ[k] V x) (g * h)) =
    HMul.hMul (α := (⨁ (i : ι), V i) →ₗ[k] ⨁ (i : ι), V i)
      (lmap (M := V) (N := V) fun (x : ι) ↦ (ρ x : (a : G) → V x →ₗ[k] V x) g)
      (lmap (M := V) (N := V) fun (x : ι) ↦ (ρ x : (a : G) → V x →ₗ[k] V x) h)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
ι : Type u_3
V : ι → Type u_4
inst_2 : (i : ι) → AddCommMonoid (V i)
inst_3 : (i : ι) → Module.{u_1, u_4} k (V i)
ρ : (i : ι) → Representation.{u_1, u_2, u_4} k G (V i)
g h : G
x : ⨁ (i : ι), V i
i : ι
⊢ (((lmap (M := V) (N := V) fun (x : ι) ↦ (ρ x : (a : G) → V x →ₗ[k] V x) (g * h) :
              (a : ⨁ (i : ι), V i) → ⨁ (i : ι), V i)
            x :
          ⨁ (i : ι), V i) :
        (a : ι) → V a)
      i =
    (((HMul.hMul (α := (⨁ (i : ι), V i) →ₗ[k] ⨁ (i : ι), V i)
                (lmap (M := V) (N := V) fun (x : ι) ↦ (ρ x : (a : G) → V x →ₗ[k] V x) g)
                (lmap (M := V) (N := V) fun (x : ι) ↦ (ρ x : (a : G) → V x →ₗ[k] V x) h) :
              (a : ⨁ (i : ι), V i) → ⨁ (i : ι), V i)
            x :
          ⨁ (i : ι), V i) :
        (a : ι) → V a)
      i

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
⊢ Eq (α := V × W →ₗ[k] V × W) (prodMap ((ρV : (a : G) → V →ₗ[k] V) 1) ((ρW : (a : G) → W →ₗ[k] W) 1)) 1

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
g h : G
⊢ prodMap ((ρV : (a : G) → V →ₗ[k] V) (g * h)) ((ρW : (a : G) → W →ₗ[k] W) (g * h)) =
    HMul.hMul (α := V × W →ₗ[k] V × W) (prodMap ((ρV : (a : G) → V →ₗ[k] V) g) ((ρW : (a : G) → W →ₗ[k] W) g))
      (prodMap ((ρV : (a : G) → V →ₗ[k] V) h) ((ρW : (a : G) → W →ₗ[k] W) h))

Tactic:
simp [prodMap_mul]

Premises used: LinearMap.prodMap_mul
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
⊢ Eq (α := V ⊗[k] W →ₗ[k] V ⊗[k] W) (map ((ρV : (a : G) → V →ₗ[k] V) 1) ((ρW : (a : G) → W →ₗ[k] W) 1)) 1

Tactic:
simp only [map_one, TensorProduct.map_one]

Premises used: TensorProduct.map_one, map_one
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
g h : G
⊢ map ((ρV : (a : G) → V →ₗ[k] V) (g * h)) ((ρW : (a : G) → W →ₗ[k] W) (g * h)) =
    HMul.hMul (α := V ⊗[k] W →ₗ[k] V ⊗[k] W) (map ((ρV : (a : G) → V →ₗ[k] V) g) ((ρW : (a : G) → W →ₗ[k] W) g))
      (map ((ρV : (a : G) → V →ₗ[k] V) h) ((ρW : (a : G) → W →ₗ[k] W) h))

Tactic:
simp only [map_mul, TensorProduct.map_mul]

Premises used: map_mul, TensorProduct.map_mul
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
⊢ Eq (α := V ⊗[k] W →ₗ[k] V ⊗[k] W) ((ρV ⊗ ρW : (a : G) → V ⊗[k] W →ₗ[k] V ⊗[k] W) g : V ⊗[k] W →ₗ[k] V ⊗[k] W)
    (map ((ρV : (a : G) → V →ₗ[k] V) g) ((ρW : (a : G) → W →ₗ[k] W) g) : V ⊗[k] W →ₗ[k] V ⊗[k] W)

Tactic:
rfl

Premises used: TensorProduct.map, TensorProduct.lift, rfl
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
r : k[G]
x : V
y : W
change :
  Eq (α := V ⊗[k] W)
    ((((asAlgebraHom (ρV ⊗ 1) : (a : k[G]) → End k (V ⊗[k] W)) r : End k (V ⊗[k] W)) : (a : V ⊗[k] W) → V ⊗[k] W)
        (have this : asModule (V := V ⊗[k] W) (ρV ⊗ 1) := x ⊗ₜ[k] y;
        this) :
      V ⊗[k] W)
    ((((ρV.asAlgebraHom : (a : k[G]) → End k V) r : End k V) : (a : V) → V)
          (have this := x;
          this) ⊗ₜ[k]
        y :
      V ⊗[k] W)
⊢ HSMul.hSMul (β := asModule (V := V ⊗[k] W) (ρV ⊗ 1)) r
      (have this : asModule (V := V ⊗[k] W) (ρV ⊗ 1) := x ⊗ₜ[k] y;
      this) =
    HSMul.hSMul (β := ρV.asModule) r
        (have this := x;
        this) ⊗ₜ[k]
      y

Tactic:
change asAlgebraHom (ρV ⊗ 1) _ _ = asAlgebraHom ρV _ _ ⊗ₜ _

Premises used: Representation.asAlgebraHom, Representation.tprod, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : AddCommMonoid W
inst_5 : Module k W
ρV : Representation k G V
r : k[G]
x : V
y : W
simp :
  Eq (α := V ⊗[k] W)
    (Finsupp.sum r fun (i : G) (d : k) ↦
      HSMul.hSMul (β := V ⊗[k] W) d ((((ρV : (a : G) → V →ₗ[k] V) i : V →ₗ[k] V) : (a : V) → V) x ⊗ₜ[k] y : V ⊗[k] W))
    ((Finsupp.sum r fun (i : G) (d : k) ↦
        HSMul.hSMul (β := V) d ((((ρV : (a : G) → V →ₗ[k] V) i : V →ₗ[k] V) : (a : V) → V) x : V)) ⊗ₜ[k]
      y)
⊢ Eq (α := V ⊗[k] W)
    ((((asAlgebraHom (ρV ⊗ 1) : (a : k[G]) → End k (V ⊗[k] W)) r : End k (V ⊗[k] W)) : (a : V ⊗[k] W) → V ⊗[k] W)
        (have this : asModule (V := V ⊗[k] W) (ρV ⊗ 1) := x ⊗ₜ[k] y;
        this) :
      V ⊗[k] W)
    ((((ρV.asAlgebraHom : (a : k[G]) → End k V) r : End k V) : (a : V) → V)
          (have this := x;
          this) ⊗ₜ[k]
        y :
      V ⊗[k] W)

Tactic:
simp only [asAlgebraHom_def, MonoidAlgebra.lift_apply, tprod_apply, MonoidHom.one_apply,
    LinearMap.finsupp_sum_apply, LinearMap.smul_apply, TensorProduct.map_tmul, Module.End.one_apply]

Premises used: Representation.asAlgebraHom_def, LinearMap.smul_apply, Representation.tprod_apply, Module.End.one_apply, LinearMap.finsupp_sum_apply, MonoidAlgebra.lift_apply, TensorProduct.map_tmul, MonoidHom.one_apply