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
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)
⊢ 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)
have 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)
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
inst_2 : Fintype G
⊢ Eq (α := Submodule k (G →₀ k)) (ker (norm (leftRegular k G))) (ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1))
have 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
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
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
⊢ Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) γ : k) ((x : (a : G) → k) g : k)
have rcases : ∀ (i : ℤ), Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) i) : k) ((x : (a : G) → k) g : k)
Tactic: rcases hg γ with ⟨i, rfl⟩
Cleared hypotheses: γ
-- 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
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 : ℤ
⊢ Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) i) : k) ((x : (a : G) → k) g : k)
have zero : Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) 0) : 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 : ℤ))
Cleared hypotheses: i
-- 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
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)
⊢ Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) i) : k) ((x : (a : G) → k) g : k)
have 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)
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 : ℤ))
Cleared hypotheses: i
-- 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
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)
⊢ Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) ((fun (x : ℤ) ↦ g ^ x) i) : k) ((x : (a : G) → k) g : k)
have 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)
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 : ℤ))
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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)
⊢ 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
have 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
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 : 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
⊢ (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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
⊢ 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
have 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)
Tactic: change asAlgebraHom (ρV ⊗ 1) _ _ = asAlgebraHom ρV _ _ ⊗ₜ _
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
⊢ 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)
have simp : Eq (α := V ⊗[k] W)
  (∑ x_1 ∈ r.support,
    HSMul.hSMul (α := k) (β := V ⊗[k] W) ((r : (a : G) → k) x_1 : k)
      ((((ρV : (a : G) → V →ₗ[k] V) x_1 : V →ₗ[k] V) : (a : V) → V) x ⊗ₜ[k] y : V ⊗[k] W))
  (∑ a ∈ r.support,
    HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V) ((r : (a : G) → k) a : k)
        ((((ρV : (a : G) → V →ₗ[k] V) a : V →ₗ[k] V) : (a : V) → V) x : V) ⊗ₜ[k]
      y)
Tactic: simp only [Finsupp.sum, TensorProduct.sum_tmul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
ρW : Representation k G W
r : k[G]
x : V
y : W
⊢ HSMul.hSMul (β := asModule (V := V ⊗[k] W) (1 ⊗ ρW)) r
      (have this : asModule (V := V ⊗[k] W) (1 ⊗ ρW) := x ⊗ₜ[k] y;
      this) =
    x ⊗ₜ[k]
      HSMul.hSMul (β := ρW.asModule) r
        (have this := y;
        this)
have change : Eq (α := V ⊗[k] W)
  ((((asAlgebraHom (1 ⊗ ρW) : (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) (1 ⊗ ρW) := x ⊗ₜ[k] y;
      this) :
    V ⊗[k] W)
  (x ⊗ₜ[k]
      (((ρW.asAlgebraHom : (a : k[G]) → End k W) r : End k W) : (a : W) → W)
        (have this := y;
        this) :
    V ⊗[k] W)
Tactic: change asAlgebraHom (1 ⊗ ρW) _ _ = _ ⊗ₜ asAlgebraHom ρW _ _
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
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
ρW : Representation k G W
r : k[G]
x : V
y : W
⊢ Eq (α := V ⊗[k] W)
    ((((asAlgebraHom (1 ⊗ ρW) : (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) (1 ⊗ ρW) := x ⊗ₜ[k] y;
        this) :
      V ⊗[k] W)
    (x ⊗ₜ[k]
        (((ρW.asAlgebraHom : (a : k[G]) → End k W) r : End k W) : (a : W) → W)
          (have this := y;
          this) :
      V ⊗[k] W)
have simp : Eq (α := V ⊗[k] W)
  (Finsupp.sum r fun (i : G) (d : k) ↦
    HSMul.hSMul (β := V ⊗[k] W) d (x ⊗ₜ[k] (((ρW : (a : G) → W →ₗ[k] W) i : W →ₗ[k] W) : (a : W) → W) y : V ⊗[k] W))
  (x ⊗ₜ[k]
    Finsupp.sum r fun (i : G) (d : k) ↦
      HSMul.hSMul (β := W) d ((((ρW : (a : G) → W →ₗ[k] W) i : W →ₗ[k] W) : (a : W) → W) y : 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]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group 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
f₁ f₂ : V →ₗ[k] W
⊢ (ρW : (a : G) → W →ₗ[k] W) g ∘ₗ (f₁ + f₂) ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹ =
    HAdd.hAdd (α := V →ₗ[k] W) ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f₁ ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)
      ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f₂ ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)
have simp_rw : (ρW : (a : G) → W →ₗ[k] W) g ∘ₗ
    HAdd.hAdd (α := V →ₗ[k] W) (f₁ ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹) (f₂ ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹) =
  HAdd.hAdd (α := V →ₗ[k] W) ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f₁ ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)
    ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f₂ ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)
Tactic: simp_rw [add_comp, comp_add]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group 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
r : k
f : V →ₗ[k] W
⊢ (ρW : (a : G) → W →ₗ[k] W) g ∘ₗ (r • f) ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹ =
    HSMul.hSMul (α := k) (β := V →ₗ[k] W) ((RingHom.id k : (a : k) → k) r : k)
      ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)
have simp_rw : (ρW : (a : G) → W →ₗ[k] W) g ∘ₗ (r • f) ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹ =
  HSMul.hSMul (β := V →ₗ[k] W) r ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)
Tactic: simp_rw [RingHom.id_apply, smul_comp, comp_smul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group 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
r : k
f : V →ₗ[k] W
simp_rw :
  (ρW : (a : G) → W →ₗ[k] W) g ∘ₗ (r • f) ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹ =
    HSMul.hSMul (β := V →ₗ[k] W) r ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)
⊢ (ρW : (a : G) → W →ₗ[k] W) g ∘ₗ (r • f) ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹ =
    HSMul.hSMul (α := k) (β := V →ₗ[k] W) ((RingHom.id k : (a : k) → k) r : k)
      ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)
have simp_rw₁ : (ρW : (a : G) → W →ₗ[k] W) g ∘ₗ HSMul.hSMul (β := V →ₗ[k] W) r (f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹) =
  HSMul.hSMul (β := V →ₗ[k] W) r ((ρW : (a : G) → W →ₗ[k] W) g ∘ₗ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)
Tactic: simp_rw [RingHom.id_apply, smul_comp, comp_smul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group 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
r : k
f : Dual k V
⊢ (r • f) ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹ =
    HSMul.hSMul (α := k) (β := Dual k V) ((RingHom.id k : (a : k) → k) r : k) (f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹)
have h : ∀ (x : V),
  Eq.{u_1 + 1} (α := k) (((r • f) ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹ : (a : V) → k) x : k)
    ((HSMul.hSMul (α := k) (β := Dual k V) ((RingHom.id k : (a : k) → k) r : k) (f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹) :
          (a : V) → k)
        x :
      k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group 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 (α := Dual k V →ₗ[k] Dual k V)
    { toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) 1⁻¹, map_add' := ⋯, map_smul' := ⋯ } 1
have h : ∀ (x : Dual k V) (x_1 : V),
  Eq.{u_1 + 1} (α := k)
    (((({ toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) 1⁻¹, map_add' := sorry, map_smul' := sorry } :
                (a : Dual k V) → Dual k V)
              x :
            Dual k V) :
          (a : V) → k)
        x_1 :
      k)
    ((((1 : (a : Dual k V) → Dual k V) x : Dual k V) : (a : V) → k) x_1 : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group 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
⊢ { toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) (g * h)⁻¹, map_add' := ⋯, map_smul' := ⋯ } =
    HMul.hMul (α := Dual k V →ₗ[k] Dual k V)
      { toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹, map_add' := ⋯, map_smul' := ⋯ :
        Dual k V →ₗ[k] Dual k V }
      { toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) h⁻¹, map_add' := ⋯, map_smul' := ⋯ :
        Dual k V →ₗ[k] Dual k V }
have h₁ : ∀ (x : Dual k V) (x_1 : V),
  Eq.{u_1 + 1} (α := k)
    (((({ toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) (g * h)⁻¹, map_add' := sorry, map_smul' := sorry } :
                (a : Dual k V) → Dual k V)
              x :
            Dual k V) :
          (a : V) → k)
        x_1 :
      k)
    ((((HMul.hMul (α := Dual k V →ₗ[k] Dual k V)
                  { toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) g⁻¹, map_add' := sorry, map_smul' := sorry :
                    Dual k V →ₗ[k] Dual k V }
                  { toFun := fun (f : Dual k V) ↦ f ∘ₗ (ρV : (a : G) → V →ₗ[k] V) h⁻¹, map_add' := sorry, map_smul' := sorry :
                    Dual k V →ₗ[k] Dual k V } :
                (a : Dual k V) → Dual k V)
              x :
            Dual k V) :
          (a : V) → k)
        x_1 :
      k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring k
inst_1 : Group 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 (α := TensorProduct k (Dual k V) W →ₗ[k] V →ₗ[k] W)
    (dualTensorHom k V W ∘ₗ
      TensorProduct.map ((ρV.dual : (a : G) → Dual k V →ₗ[k] Dual k V) g) ((ρW : (a : G) → W →ₗ[k] W) g))
    ((ρV.linHom ρW : (a : G) → (V →ₗ[k] W) →ₗ[k] V →ₗ[k] W) g ∘ₗ dualTensorHom k V W)
have a : ∀ (x : Dual k V) (x_1 : W) (x_2 : V),
  Eq.{u_4 + 1} (α := W)
    (((((((TensorProduct.AlgebraTensorModule.curry
                          (dualTensorHom k V W ∘ₗ
                            TensorProduct.map ((ρV.dual : (a : G) → Dual k V →ₗ[k] Dual k V) g)
                              ((ρW : (a : G) → W →ₗ[k] W) g)) :
                        Dual k V →ₗ[k] W →ₗ[k] V →ₗ[k] W) :
                      (a : Dual k V) → W →ₗ[k] V →ₗ[k] W)
                    x :
                  W →ₗ[k] V →ₗ[k] W) :
                (a : W) → V →ₗ[k] W)
              x_1 :
            V →ₗ[k] W) :
          (a : V) → W)
        x_2 :
      W)
    (((((((TensorProduct.AlgebraTensorModule.curry
                          ((ρV.linHom ρW : (a : G) → (V →ₗ[k] W) →ₗ[k] V →ₗ[k] W) g ∘ₗ dualTensorHom k V W) :
                        Dual k V →ₗ[k] W →ₗ[k] V →ₗ[k] W) :
                      (a : Dual k V) → W →ₗ[k] V →ₗ[k] W)
                    x :
                  W →ₗ[k] V →ₗ[k] W) :
                (a : W) → V →ₗ[k] W)
              x_1 :
            V →ₗ[k] W) :
          (a : V) → W)
        x_2 :
      W)
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 : Monoid G
α_1 : Type u_3
A : Type u_4
B : Type u_5
inst_2 : AddCommMonoid A
inst_3 : Module k A
ρ : Representation k G A
inst_4 : AddCommMonoid B
inst_5 : Module k B
τ : Representation k G B
α : Type u_6
x_1 : k[G]
x : α →₀ k[G]
⊢ Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl (α →₀ k[G]))) (x_1 • x) =
    HSMul.hSMul (α := k[G]) ((RingHom.id k[G] : (a : k[G]) → k[G]) x_1 : k[G])
      (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl (α →₀ k[G]))) x)
have simp : x_1 • x = x_1 • x
Tactic: simp only [AddEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe,
        AddEquiv.refl_apply, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
α_1 : Type u_3
A : Type u_4
B : Type u_5
inst_2 : AddCommMonoid A
inst_3 : Module k A
ρ : Representation k G A
inst_4 : AddCommMonoid B
inst_5 : Module k B
τ : Representation k G B
α : Type u_6
x : k[G]
a : α
b : k[G]
f : α →₀ k[G]
h_1 : a ∉ f.support
h_2 : b ≠ 0
h : x • f = x • f
⊢ x • (Finsupp.single a b + f) = x • (Finsupp.single a b + f)
have single_add : HSMul.hSMul (β := α →₀ k[G]) x (Finsupp.single a b) + x • f = x • (Finsupp.single a b + f)
Tactic: rw [smul_add, h]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
α_1 : Type u_3
A : Type u_4
B : Type u_5
inst_2 : AddCommMonoid A
inst_3 : Module k A
ρ : Representation k G A
inst_4 : AddCommMonoid B
inst_5 : Module k B
τ : Representation k G B
α : Type u_6
x : k[G]
a : α
b : k[G]
f : α →₀ k[G]
h_1 : a ∉ f.support
h_2 : b ≠ 0
h : x • f = x • f
⊢ HSMul.hSMul (β := α →₀ k[G]) x (Finsupp.single a b) + x • f = x • (Finsupp.single a b + f)
have single_add : HAdd.hAdd (β := α →₀ k[G]) (HSMul.hSMul (β := α →₀ k[G]) x (Finsupp.single a b))
    ((((asAlgebraHom (free k G α) : (a : k[G]) → End k (α →₀ k[G])) x : End k (α →₀ k[G])) :
          (a : α →₀ k[G]) → α →₀ k[G])
        f :
      α →₀ k[G]) =
  (((asAlgebraHom (free k G α) : (a : k[G]) → End k (free k G α).asModule) x :
        End k (asModule (V := α →₀ G →₀ k) (free k G α))) :
      (a : (free k G α).asModule) → (free k G α).asModule)
    (Finsupp.single a b + f)
Tactic: change _ + asAlgebraHom _ _ _ = asAlgebraHom _ _ _