awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Ring k
inst_1 : Monoid G
I : AddCommGroup V
inst_2 : Module k V
ρ : Representation k G V
g : G
x : V
n : ℕ
h :
  (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
      (Fin.partialSum (n := n + 1)
        (fun (j : Fin (n + 1)) ↦ (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x)
        (Fin.last (n + 1))) =
    HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (n + 1)) : V →ₗ[k] V) : (a : V) → V) x : V) x
⊢ Eq.{u_3 + 1} (α := (i : Fin (n + 1)) → V)
    (Fin.init (α := fun (j : Fin (n + 2)) ↦ V) fun (j : Fin (n + 2)) ↦
        (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x :
      (i : Fin (n + 1)) → V)
    fun (j : Fin (n + 1)) ↦ ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x : V)

Tactic:
have : Fin.init (fun (j : Fin (n + 2)) => ρ (g ^ (j : ℕ)) x) =
      fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) x := by ext; simp [Fin.init]
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Ring k
inst_1 : Monoid G
I : AddCommGroup V
inst_2 : Module k V
ρ : Representation k G V
g : G
x : V
n : ℕ
h :
  (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
      (Fin.partialSum (n := n + 1)
        (fun (j : Fin (n + 1)) ↦ (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x)
        (Fin.last (n + 1))) =
    HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (n + 1)) : V →ₗ[k] V) : (a : V) → V) x : V) x
this :
  Eq.{u_3 + 1} (α := (i : Fin (n + 1)) → V)
    (Fin.init (α := fun (j : Fin (n + 2)) ↦ V) fun (j : Fin (n + 2)) ↦
        (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x :
      (i : Fin (n + 1)) → V)
    fun (j : Fin (n + 1)) ↦ ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x : V)
succ :
  HAdd.hAdd (β := V)
      (HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (n + 1)) : V →ₗ[k] V) : (a : V) → V) x : V) x)
      ((HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id :
            (a : V) → V)
          ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑(Fin.last (n + 1)) : ℕ)) : V →ₗ[k] V) : (a : V) → V) x : V) :
        V) =
    HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (n + 1 + 1)) : V →ₗ[k] V) : (a : V) → V) x : V) x
⊢ (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
      (Fin.partialSum (n := n + 1 + 1)
        (fun (j : Fin (n + 1 + 1)) ↦ (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x)
        (Fin.last (n + 1 + 1))) =
    HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (n + 1 + 1)) : V →ₗ[k] V) : (a : V) → V) x : V) x

Tactic:
rw [← Fin.succ_eq_last_succ.2 rfl, Fin.partialSum_succ, ← Fin.partialSum_init, map_add,
      this, h]

Premises used: Iff.mpr, map_add, Fin.succ_eq_last_succ, Fin.partialSum_init, Fin.partialSum_succ, rfl
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Ring k
inst_1 : Monoid G
I : AddCommGroup V
inst_2 : Module k V
ρ : Representation k G V
g : G
x : V
n : ℕ
h :
  (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
      (Fin.partialSum (n := n + 1)
        (fun (j : Fin (n + 1)) ↦ (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x)
        (Fin.last (n + 1))) =
    HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (n + 1)) : V →ₗ[k] V) : (a : V) → V) x : V) x
this :
  Eq.{u_3 + 1} (α := (i : Fin (n + 1)) → V)
    (Fin.init (α := fun (j : Fin (n + 2)) ↦ V) fun (j : Fin (n + 2)) ↦
        (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x :
      (i : Fin (n + 1)) → V)
    fun (j : Fin (n + 1)) ↦ ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x : V)
⊢ HAdd.hAdd (β := V)
      (HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (n + 1)) : V →ₗ[k] V) : (a : V) → V) x : V) x)
      ((HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id :
            (a : V) → V)
          ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑(Fin.last (n + 1)) : ℕ)) : V →ₗ[k] V) : (a : V) → V) x : V) :
        V) =
    HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (n + 1 + 1)) : V →ₗ[k] V) : (a : V) → V) x : V) x

Tactic:
simp [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Ring k
inst_1 : Monoid G
I : AddCommGroup V
inst_2 : Module k V
ρ : Representation k G V
n : ℕ
g : G
x : V
zero :
  (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
      (Fin.partialSum (n := HAdd.hAdd (α := ℕ) 0 1)
        (fun (j : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦
          (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x)
        (Fin.last (HAdd.hAdd (α := ℕ) 0 1))) =
    HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (g ^ HAdd.hAdd (α := ℕ) 0 1) : V →ₗ[k] V) : (a : V) → V) x : V) x
succ :
  ∀ (n : ℕ)
    (h :
      (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
          (Fin.partialSum (n := n + 1)
            (fun (j : Fin (n + 1)) ↦ (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x)
            (Fin.last (n + 1))) =
        HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (n + 1)) : V →ₗ[k] V) : (a : V) → V) x : V) x),
    (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
        (Fin.partialSum (n := n + 1 + 1)
          (fun (j : Fin (n + 1 + 1)) ↦ (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x)
          (Fin.last (n + 1 + 1))) =
      HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (n + 1 + 1)) : V →ₗ[k] V) : (a : V) → V) x : V) x
⊢ (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
      (Fin.partialSum (n := n + 1)
        (fun (j : Fin (n + 1)) ↦ (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x)
        (Fin.last (n + 1))) =
    HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (n + 1)) : V →ₗ[k] V) : (a : V) → V) x : V) x

Tactic:
induction n with
  | zero => simp [Fin.partialSum]
  | succ n h =>
    have : Fin.init (fun (j : Fin (n + 2)) => ρ (g ^ (j : ℕ)) x) =
      fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) x := by ext; simp [Fin.init]
    rw [← Fin.succ_eq_last_succ.2 rfl, Fin.partialSum_succ, ← Fin.partialSum_init, map_add,
      this, h]
    simp [pow_succ']

Premises used: Iff.mpr, map_add, Fin.succ_eq_last_succ, Fin.partialSum_init, Fin.partialSum_succ, Fin.partialSum, pow_succ', rfl
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
inst : Semiring k
G : Type u_2
inst_1 : Monoid G
H : Type u_3
inst_2 : MulAction G H
h :
  ∀ (x y : H),
    Eq.{u_1 + 1} (α := k)
      ((((Finsupp.lmapDomain k k fun (x : H) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := G) 1 x) ∘ₗ Finsupp.lsingle x :
                (a : k) → H →₀ k)
              1 :
            (a : H) → k)
          y :
        k)
      (((1 ∘ₗ Finsupp.lsingle x : (a : k) → H →₀ k) 1 : (a : H) → k) y : k)
⊢ Eq (α := (H →₀ k) →ₗ[k] H →₀ k) (Finsupp.lmapDomain k k fun (x : H) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := G) 1 x) 1

Tactic:
ext x y
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
inst : Semiring k
G : Type u_2
inst_1 : Monoid G
H : Type u_3
inst_2 : MulAction G H
x y : H
⊢ Eq.{u_1 + 1} (α := k)
    ((((Finsupp.lmapDomain k k fun (x : H) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := G) 1 x) ∘ₗ Finsupp.lsingle x :
              (a : k) → H →₀ k)
            1 :
          (a : H) → k)
        y :
      k)
    (((1 ∘ₗ Finsupp.lsingle x : (a : k) → H →₀ k) 1 : (a : H) → k) y : k)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
inst : Semiring k
G : Type u_2
inst_1 : Monoid G
H : Type u_3
inst_2 : MulAction G H
x y : G
h :
  ∀ (z w : H),
    Eq.{u_1 + 1} (α := k)
      ((((Finsupp.lmapDomain k k fun (x_1 : H) ↦ (x * y) • x_1) ∘ₗ Finsupp.lsingle z : (a : k) → H →₀ k) 1 :
            (a : H) → k)
          w :
        k)
      (((HMul.hMul (α := (H →₀ k) →ₗ[k] H →₀ k) (Finsupp.lmapDomain k k fun (x_1 : H) ↦ x • x_1)
                    (Finsupp.lmapDomain k k fun (x : H) ↦ y • x) ∘ₗ
                  Finsupp.lsingle z :
                (a : k) → H →₀ k)
              1 :
            (a : H) → k)
          w :
        k)
⊢ (Finsupp.lmapDomain k k fun (x_1 : H) ↦ (x * y) • x_1) =
    HMul.hMul (α := (H →₀ k) →ₗ[k] H →₀ k) (Finsupp.lmapDomain k k fun (x_1 : H) ↦ x • x_1)
      (Finsupp.lmapDomain k k fun (x : H) ↦ y • x)

Tactic:
ext z w
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
inst : Semiring k
G : Type u_2
inst_1 : Monoid G
H : Type u_3
inst_2 : MulAction G H
x y : G
z w : H
⊢ Eq.{u_1 + 1} (α := k)
    ((((Finsupp.lmapDomain k k fun (x_1 : H) ↦ (x * y) • x_1) ∘ₗ Finsupp.lsingle z : (a : k) → H →₀ k) 1 : (a : H) → k)
        w :
      k)
    (((HMul.hMul (α := (H →₀ k) →ₗ[k] H →₀ k) (Finsupp.lmapDomain k k fun (x_1 : H) ↦ x • x_1)
                  (Finsupp.lmapDomain k k fun (x : H) ↦ y • x) ∘ₗ
                Finsupp.lsingle z :
              (a : k) → H →₀ k)
            1 :
          (a : H) → k)
        w :
      k)

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
inst : Semiring k
G : Type u_2
inst_1 : Monoid G
H : Type u_3
inst_2 : MulAction G H
g : G
⊢ Eq (α := (H →₀ k) →ₗ[k] H →₀ k) ((ofMulAction k G H : (a : G) → (H →₀ k) →ₗ[k] H →₀ k) g : (H →₀ k) →ₗ[k] H →₀ k)
    (Finsupp.lmapDomain k k fun (x : H) ↦ g • x : (H →₀ k) →ₗ[k] H →₀ k)

Tactic:
rfl

Premises used: Finsupp.lmapDomain, rfl
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
inst : Semiring k
G : Type u_2
inst_1 : Monoid G
H : Type u_3
inst_2 : MulAction G H
g : G
x : H
r : k
⊢ Eq (α := H →₀ k)
    ((((ofMulAction k G H : (a : G) → (H →₀ k) →ₗ[k] H →₀ k) g : (H →₀ k) →ₗ[k] H →₀ k) : (a : H →₀ k) → H →₀ k)
        (Finsupp.single x r) :
      H →₀ k)
    (Finsupp.single (g • x) r : H →₀ k)

Tactic:
Finsupp.mapDomain_single

Premises used: Multiset.sum, Multiset.foldr, Finsupp.mapDomain, Finsupp.sum, Finsupp.mapDomain_single, Finset.sum
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
A : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
h :
  ∀ (x : A),
    Eq (α := A)
      ((let __src : AddMonoid.End A :=
              ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) :
                  (a : G) → AddMonoid.End A)
                1;
            { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ } :
            (a : A) → A)
          x :
        A)
      ((1 : (a : A) → A) x : A)
⊢ Eq.{u_3 + 1} (α := A →ₗ[k] A)
    (let __src : AddMonoid.End A :=
      ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) : (a : G) → AddMonoid.End A) 1;
    { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ })
    1

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
A : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
x : A
⊢ Eq (α := A)
    ((let __src : AddMonoid.End A :=
            ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) :
                (a : G) → AddMonoid.End A)
              1;
          { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ } :
          (a : A) → A)
        x :
      A)
    ((1 : (a : A) → A) x : A)

Tactic:
one_smul _ _

Premises used: one_smul
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
A : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
x : A
⊢ Eq (α := A)
    ((let __src : AddMonoid.End A :=
            ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) :
                (a : G) → AddMonoid.End A)
              1;
          { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ } :
          (a : A) → A)
        x :
      A)
    ((1 : (a : A) → A) x : A)

Tactic:
exact one_smul _ _

Premises used: one_smul
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
A : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
x y : G
h :
  ∀ (x_1 : A),
    Eq (α := A)
      ((let __src : AddMonoid.End A :=
              ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) :
                  (a : G) → AddMonoid.End A)
                (x * y);
            { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ } :
            (a : A) → A)
          x_1 :
        A)
      ((HMul.hMul (α := A →ₗ[k] A)
              (let __src : AddMonoid.End A :=
                ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) :
                    (a : G) → AddMonoid.End A)
                  x;
              { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[k] A })
              (let __src : AddMonoid.End A :=
                ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) :
                    (a : G) → AddMonoid.End A)
                  y;
              { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[k] A }) :
            (a : A) → A)
          x_1 :
        A)
⊢ (let __src : AddMonoid.End A :=
      ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) : (a : G) → AddMonoid.End A)
        (x * y);
    { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ }) =
    HMul.hMul (α := A →ₗ[k] A)
      (let __src : AddMonoid.End A :=
        ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) : (a : G) → AddMonoid.End A)
          x;
      { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[k] A })
      (let __src : AddMonoid.End A :=
        ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) : (a : G) → AddMonoid.End A)
          y;
      { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[k] A })

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
A : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
x y : G
x_1 : A
⊢ Eq (α := A)
    ((let __src : AddMonoid.End A :=
            ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) :
                (a : G) → AddMonoid.End A)
              (x * y);
          { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ } :
          (a : A) → A)
        x_1 :
      A)
    ((HMul.hMul (α := A →ₗ[k] A)
            (let __src : AddMonoid.End A :=
              ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) :
                  (a : G) → AddMonoid.End A)
                x;
            { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[k] A })
            (let __src : AddMonoid.End A :=
              ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) :
                  (a : G) → AddMonoid.End A)
                y;
            { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[k] A }) :
          (a : A) → A)
        x_1 :
      A)

Tactic:
mul_smul _ _ _

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
A : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
x y : G
x_1 : A
⊢ Eq (α := A)
    ((let __src : AddMonoid.End A :=
            ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) :
                (a : G) → AddMonoid.End A)
              (x * y);
          { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ } :
          (a : A) → A)
        x_1 :
      A)
    ((HMul.hMul (α := A →ₗ[k] A)
            (let __src : AddMonoid.End A :=
              ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) :
                  (a : G) → AddMonoid.End A)
                x;
            { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[k] A })
            (let __src : AddMonoid.End A :=
              ((DistribMulAction.toAddMonoidEnd G A : MonoidHom.{u_2, u_3} G (AddMonoid.End A)) :
                  (a : G) → AddMonoid.End A)
                y;
            { toFun := (↑__src : ZeroHom A A).toFun, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[k] A }) :
          (a : A) → A)
        x_1 :
      A)

Tactic:
exact mul_smul _ _ _

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
A : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
g : G
a : A
⊢ ((((ofDistribMulAction k G A : Representation k G A) : (a : G) → A →ₗ[k] A) g : A →ₗ[k] A) : (a : A) → A) a = g • a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
A : Type u_3
inst : Semiring k
inst_1 : AddCommMonoid A
inst_2 : Module k A
G : Type u_4
inst_3 : Group G
inst_4 : Fintype G
inst_5 : DistribMulAction G A
inst_6 : SMulCommClass G k A
x : A
⊢ Eq (α := A) ((norm (ofDistribMulAction k G A) : (a : A) → A) x : A) (∑ g : G, g • x : A)

Tactic:
simp [norm]

Premises used: Representation.norm
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
M : Type u_1
G : Type u_2
inst : Monoid M
inst_1 : CommGroup G
inst_2 : MulDistribMulAction M G
g : M
a : Additive G
⊢ Eq (α := Additive G)
    (((((ofMulDistribMulAction M G : Representation.{0, u_1, u_2} ℤ M (Additive G)) :
                (a : M) → Additive G →ₗ[ℤ] Additive G)
              g :
            Additive G →ₗ[ℤ] Additive G) :
          (a : Additive G) → Additive G)
        a :
      Additive G)
    ((Additive.ofMul : (a : G) → Additive G) (HSMul.hSMul (β := G) g ((Additive.toMul : (a : Additive G) → G) a : G)) :
      Additive G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
G M : Type
inst : Group G
inst_1 : Fintype G
inst_2 : CommGroup M
inst_3 : MulDistribMulAction G M
x : Additive M
⊢ Eq (α := M)
    ((Additive.toMul : (a : Additive M) → M)
        ((norm (ofMulDistribMulAction G M) : (a : Additive M) → Additive M) x : Additive M) :
      M)
    (∏ g : G, HSMul.hSMul (β := M) g ((Additive.toMul : (a : Additive M) → M) x : M) : M)

Tactic:
simp [norm]

Premises used: Representation.norm
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
H : Type u_4
inst_2 : MulAction G H
g : G
f : H →₀ k
h : H
rw :
  ((((((ofMulAction k G H : (a : G) → (H →₀ k) →ₗ[k] H →₀ k) g : (H →₀ k) →ₗ[k] H →₀ k) : (a : H →₀ k) → H →₀ k) f :
          H →₀ k) :
        (a : H) → k)
      (g • g⁻¹ • h) :
    k)
| ((((((ofMulAction k G H : (a : G) → (H →₀ k) →ₗ[k] H →₀ k) g : (H →₀ k) →ₗ[k] H →₀ k) : (a : H →₀ k) → H →₀ k) f :
          H →₀ k) :
        (a : H) → k)
      h :
    k)

Tactic:
rw [← smul_inv_smul g h]

Premises used: smul_inv_smul
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
H : Type u_4
inst_2 : MulAction G H
g : G
f : H →₀ k
h : H
conv_lhs :
  Eq.{u_1 + 1} (α := k)
    ((((((ofMulAction k G H : (a : G) → (H →₀ k) →ₗ[k] H →₀ k) g : (H →₀ k) →ₗ[k] H →₀ k) : (a : H →₀ k) → H →₀ k) f :
            H →₀ k) :
          (a : H) → k)
        (g • g⁻¹ • h) :
      k)
    ((f : (a : H) → k) (g⁻¹ • h) : k)
⊢ Eq.{u_1 + 1} (α := k)
    ((((((ofMulAction k G H : (a : G) → (H →₀ k) →ₗ[k] H →₀ k) g : (H →₀ k) →ₗ[k] H →₀ k) : (a : H →₀ k) → H →₀ k) f :
            H →₀ k) :
          (a : H) → k)
        h :
      k)
    ((f : (a : H) → k) (g⁻¹ • h) : k)

Tactic:
conv_lhs => rw [← smul_inv_smul g h]

Premises used: smul_inv_smul
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
H : Type u_4
inst_2 : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
change :
  Eq.{u_1 + 1} (α := k)
    ((((((ofMulAction k G H : (a : G) → (H →₀ k) →ₗ[k] H →₀ k) g : (H →₀ k) →ₗ[k] H →₀ k) : (a : H →₀ k) → H →₀ k) f :
            H →₀ k) :
          (a : H) → k)
        (g • h') :
      k)
    ((f : (a : H) → k) h' : k)
⊢ Eq.{u_1 + 1} (α := k)
    ((((((ofMulAction k G H : (a : G) → (H →₀ k) →ₗ[k] H →₀ k) g : (H →₀ k) →ₗ[k] H →₀ k) : (a : H →₀ k) → H →₀ k) f :
            H →₀ k) :
          (a : H) → k)
        (g • g⁻¹ • h) :
      k)
    ((f : (a : H) → k) (g⁻¹ • h) : k)

Tactic:
change ofMulAction k G H g f (g • h') = f h'

Premises used: Representation.ofMulAction, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
H : Type u_4
inst_2 : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
h₁ h₂ : H
⊢ Eq.{u_4 + 1} (α := H) ((fun (x : H) ↦ g • x) h₁) ((fun (x : H) ↦ g • x) h₂) → h₁ = h₂

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
H : Type u_4
inst_2 : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
⊢ Function.Injective (β := H) fun (x : H) ↦ g • x

Tactic:
have hg : Function.Injective (g • · : H → H) := by
    intro h₁ h₂
    simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
H : Type u_4
inst_2 : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
hg : Function.Injective (β := H) fun (x : H) ↦ g • x
⊢ Eq.{u_1 + 1} (α := k)
    ((((((ofMulAction k G H : (a : G) → (H →₀ k) →ₗ[k] H →₀ k) g : (H →₀ k) →ₗ[k] H →₀ k) : (a : H →₀ k) → H →₀ k) f :
            H →₀ k) :
          (a : H) → k)
        (g • h') :
      k)
    ((f : (a : H) → k) h' : k)

Tactic:
simp only [ofMulAction_def, Finsupp.lmapDomain_apply, Finsupp.mapDomain_apply, hg]

Premises used: Finsupp.mapDomain_apply, Finsupp.lmapDomain_apply, Representation.ofMulAction_def
-- 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 : G
hM :
  ∀ (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)
⊢ (((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 =
    HMul.hMul (α := k[G]) ((of k G : (a : G) → k[G]) g : k[G]) y

Tactic:
ext