awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_4 : S.Normal
inst_5 : IsTrivial (MonoidHom.comp ρ S.subtype)
y : G
z : Gᵐᵒᵖ
hz : z ∈ S.op
⊢ (Con.ker ρ : (a : G) → G → Prop) ((fun (m : ↥S.op) ↦ m • y) (Subtype.mk (p := fun (x : Gᵐᵒᵖ) ↦ x ∈ S.op) z hz)) y
have h : ∀ (w : V),
  Eq (α := V)
    (((ρ : (a : G) → V →ₗ[k] V) ((fun (m : ↥S.op) ↦ m • y) (Subtype.mk (p := fun (x : Gᵐᵒᵖ) ↦ x ∈ S.op) z hz)) :
          (a : V) → V)
        w :
      V)
    ((((ρ : (a : G) → V →ₗ[k] V) y : V →ₗ[k] V) : (a : V) → V) w : V)
Tactic: ext w
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_4 : S.Normal
inst_5 : IsTrivial (MonoidHom.comp ρ S.subtype)
y : G
z : Gᵐᵒᵖ
hz : z ∈ S.op
w : V
⊢ Eq (α := V)
    (((ρ : (a : G) → V →ₗ[k] V) ((fun (m : ↥S.op) ↦ m • y) (Subtype.mk (p := fun (x : Gᵐᵒᵖ) ↦ x ∈ S.op) z hz)) :
          (a : V) → V)
        w :
      V)
    ((((ρ : (a : G) → V →ₗ[k] V) y : V →ₗ[k] V) : (a : V) → V) w : V)
have h : Eq (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (y * MulOpposite.unop z) : V →ₗ[k] V) : (a : V) → V) w : V)
  ((((ρ : (a : G) → V →ₗ[k] V) y : V →ₗ[k] V) : (a : V) → V) w : V)
Tactic: change ρ (_ * z.unop) _ = _
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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)
have h₁ : ∀ (x_1 : Fin (n + 1)),
  Eq.{u_3 + 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) x_1 :
      V)
    ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑x_1 : ℕ)) : V →ₗ[k] V) : (a : V) → V) x : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (hypothesis)
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
⊢ (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
have 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)
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]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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)
⊢ (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
have 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
Tactic: rw [← Fin.succ_eq_last_succ.2 rfl, Fin.partialSum_succ, ← Fin.partialSum_init, map_add,
      this, h]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
⊢ (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
have 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
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']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
⊢ (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
have 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
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']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
⊢ 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
have 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: ext x y
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
⊢ (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)
have 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)
Tactic: ext z w
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
⊢ 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
have 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' := sorry, map_smul' := sorry } :
          (a : A) → A)
        x :
      A)
    ((1 : (a : A) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
⊢ (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 })
have 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' := sorry, map_smul' := sorry } :
          (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' := sorry, map_smul' := sorry : 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' := sorry, map_smul' := sorry : A →ₗ[k] A }) :
          (a : A) → A)
        x_1 :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
| ((((((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)
have 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)
Tactic: rw [← smul_inv_smul g h]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
⊢ 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)
have 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)
Tactic: conv_lhs => rw [← smul_inv_smul g h]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (hypothesis)
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
⊢ 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)
have hg : Function.Injective (β := H) fun (x : H) ↦ g • x
Tactic: have hg : Function.Injective (g • · : H → H) := by
    intro h₁ h₂
    simp
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
⊢ (((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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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)
⊢ x • y = x * y
have 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
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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
⊢ x • y = x * y
have 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
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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
⊢ x • y = x * y
have hsmul : ∀ (r : k) (x : k[G]) (hx : x • y = x * y), (r • x) • y = r • 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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
⊢ 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
have 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)
Tactic: ext i : 2
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
x : G →₀ 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)
have 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)
Tactic: rw [leftRegular_norm_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
x : 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: constructor