awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
f : ρ.IntertwiningMap ρ
n : ℕ
zero :
  (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (HPow.hPow (β := ℕ) f 0) =
    HPow.hPow (α := V →ₗ[A] V) (β := ℕ) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) 0
⊢ (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (f ^ n) =
    HPow.hPow (α := V →ₗ[A] V) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) n
have succ : ∀ (n : ℕ)
  (ih :
    (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (f ^ n) =
      HPow.hPow (α := V →ₗ[A] V) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) n),
  (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (f ^ (n + 1)) =
    HPow.hPow (α := V →ₗ[A] V) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) (n + 1)
Tactic: induction n with
      | zero => rfl
      | succ n ih => simp [ih, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
a : A
f g : ρ.IntertwiningMap ρ
⊢ f * a • g = a • (f * g)
have h : ∀ (x : V), Eq (α := V) (((f * a • g).toLinearMap : (a : V) → V) x : V) (((a • (f * g)).toLinearMap : (a : V) → V) x : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
g : G
hg : Membership.mem (γ := Submonoid G) (Submonoid.center G) g
⊢ ρ.IsIntertwiningMap ρ ((ρ : (a : G) → V →ₗ[A] V) g)
have rw : ∀ (g_1 : G) (v : V),
  Eq (α := V)
    ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g_1 : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
    ((((ρ : (a : G) → V →ₗ[A] V) g_1 : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
Tactic: rw [isIntertwiningMap_iff]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
g : G
hg : Membership.mem (γ := Submonoid G) (Submonoid.center G) g
g' : G
v : V
⊢ Eq (α := V)
    ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
    ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
have rw : ∀ (hg : ∀ (g_1 : G), g_1 * g = g * g_1) (g' : G) (v : V),
  Eq (α := V)
    ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
    ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
Tactic: rw [Submonoid.mem_center_iff] at hg
Cleared hypotheses: hg, g', v
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
g : G
hg : ∀ (g_1 : G), g_1 * g = g * g_1
g' : G
v : V
⊢ Eq (α := V)
    ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
    ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
have rw : Eq (α := V)
  ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V)
          ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) :
        (a : V) → V)
      v :
    V)
  ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
      ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
    V)
Tactic: rw [← Module.End.mul_apply, ← Module.End.mul_apply, ← ρ.map_mul, ← hg g', ρ.map_mul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
g : G
hg : ∀ (g_1 : G), g_1 * g = g * g_1
g' : G
v : V
rw :
  Eq (α := V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
    ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
⊢ Eq (α := V)
    ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
    ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
have rw₁ : Eq (α := V)
  ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V)
          ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) :
        (a : V) → V)
      v :
    V)
  ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
          ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
        (a : V) → V)
      v :
    V)
Tactic: rw [← Module.End.mul_apply, ← Module.End.mul_apply, ← ρ.map_mul, ← hg g', ρ.map_mul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
g : G
hg : ∀ (g_1 : G), g_1 * g = g * g_1
g' : G
v : V
rw :
  Eq (α := V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
    ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
rw₁ :
  Eq (α := V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
⊢ Eq (α := V)
    ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
    ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
have rw₂ : Eq (α := V) ((((ρ : (a : G) → V →ₗ[A] V) (g * g') : V →ₗ[A] V) : (a : V) → V) v : V)
  ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
          ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
        (a : V) → V)
      v :
    V)
Tactic: rw [← Module.End.mul_apply, ← Module.End.mul_apply, ← ρ.map_mul, ← hg g', ρ.map_mul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
g : G
hg : ∀ (g_1 : G), g_1 * g = g * g_1
g' : G
v : V
rw :
  Eq (α := V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
    ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
rw₁ :
  Eq (α := V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
rw₂ :
  Eq (α := V) ((((ρ : (a : G) → V →ₗ[A] V) (g * g') : V →ₗ[A] V) : (a : V) → V) v : V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
⊢ Eq (α := V)
    ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
    ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
have rw₃ : Eq (α := V) ((((ρ : (a : G) → V →ₗ[A] V) (g' * g) : V →ₗ[A] V) : (a : V) → V) v : V)
  ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
          ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
        (a : V) → V)
      v :
    V)
Tactic: rw [← Module.End.mul_apply, ← Module.End.mul_apply, ← ρ.map_mul, ← hg g', ρ.map_mul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
g : G
hg : ∀ (g_1 : G), g_1 * g = g * g_1
g' : G
v : V
rw :
  Eq (α := V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
    ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
rw₁ :
  Eq (α := V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
rw₂ :
  Eq (α := V) ((((ρ : (a : G) → V →ₗ[A] V) (g * g') : V →ₗ[A] V) : (a : V) → V) v : V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
rw₃ :
  Eq (α := V) ((((ρ : (a : G) → V →ₗ[A] V) (g' * g) : V →ₗ[A] V) : (a : V) → V) v : V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
⊢ Eq (α := V)
    ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
    ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
have rw₄ : Eq (α := V)
  ((HMul.hMul (α := V →ₗ[A] V) (β := V →ₗ[A] V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
          ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
        (a : V) → V)
      v :
    V)
  ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
          ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
        (a : V) → V)
      v :
    V)
Tactic: rw [← Module.End.mul_apply, ← Module.End.mul_apply, ← ρ.map_mul, ← hg g', ρ.map_mul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x : G
⊢ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ
      (ρ.tprod τ : (a : G) → TensorProduct A V U →ₗ[A] TensorProduct A V U) x =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
have rw : TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ
    TensorProduct.map ((ρ : (a : G) → V →ₗ[A] V) x) ((τ : (a : G) → U →ₗ[A] U) x) =
  (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
    TensorProduct.map f.toLinearMap g.toLinearMap
Tactic: rw [tprod_apply, ← TensorProduct.map_comp, f.2, g.2, TensorProduct.map_comp, tprod_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x : G
rw :
  TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ
      TensorProduct.map ((ρ : (a : G) → V →ₗ[A] V) x) ((τ : (a : G) → U →ₗ[A] U) x) =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
⊢ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ
      (ρ.tprod τ : (a : G) → TensorProduct A V U →ₗ[A] TensorProduct A V U) x =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
have rw₁ : TensorProduct.map (f.toLinearMap ∘ₗ (ρ : (a : G) → V →ₗ[A] V) x) (g.toLinearMap ∘ₗ (τ : (a : G) → U →ₗ[A] U) x) =
  (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
    TensorProduct.map f.toLinearMap g.toLinearMap
Tactic: rw [tprod_apply, ← TensorProduct.map_comp, f.2, g.2, TensorProduct.map_comp, tprod_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x : G
rw :
  TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ
      TensorProduct.map ((ρ : (a : G) → V →ₗ[A] V) x) ((τ : (a : G) → U →ₗ[A] U) x) =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
rw₁ :
  TensorProduct.map (f.toLinearMap ∘ₗ (ρ : (a : G) → V →ₗ[A] V) x) (g.toLinearMap ∘ₗ (τ : (a : G) → U →ₗ[A] U) x) =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
⊢ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ
      (ρ.tprod τ : (a : G) → TensorProduct A V U →ₗ[A] TensorProduct A V U) x =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
have rw₂ : Eq (α := TensorProduct A V U →ₗ[A] TensorProduct A W P)
  (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x ∘ₗ f.toLinearMap) (g.toLinearMap ∘ₗ (τ : (a : G) → U →ₗ[A] U) x))
  ((σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
    TensorProduct.map f.toLinearMap g.toLinearMap)
Tactic: rw [tprod_apply, ← TensorProduct.map_comp, f.2, g.2, TensorProduct.map_comp, tprod_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x : G
rw :
  TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ
      TensorProduct.map ((ρ : (a : G) → V →ₗ[A] V) x) ((τ : (a : G) → U →ₗ[A] U) x) =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
rw₁ :
  TensorProduct.map (f.toLinearMap ∘ₗ (ρ : (a : G) → V →ₗ[A] V) x) (g.toLinearMap ∘ₗ (τ : (a : G) → U →ₗ[A] U) x) =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
rw₂ :
  Eq (α := TensorProduct A V U →ₗ[A] TensorProduct A W P)
    (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x ∘ₗ f.toLinearMap) (g.toLinearMap ∘ₗ (τ : (a : G) → U →ₗ[A] U) x))
    ((σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap)
⊢ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ
      (ρ.tprod τ : (a : G) → TensorProduct A V U →ₗ[A] TensorProduct A V U) x =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
have rw₃ : Eq (α := TensorProduct A V U →ₗ[A] TensorProduct A W P)
  (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x ∘ₗ f.toLinearMap) ((π : (a : G) → P →ₗ[A] P) x ∘ₗ g.toLinearMap))
  ((σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
    TensorProduct.map f.toLinearMap g.toLinearMap)
Tactic: rw [tprod_apply, ← TensorProduct.map_comp, f.2, g.2, TensorProduct.map_comp, tprod_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x : G
rw :
  TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ
      TensorProduct.map ((ρ : (a : G) → V →ₗ[A] V) x) ((τ : (a : G) → U →ₗ[A] U) x) =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
rw₁ :
  TensorProduct.map (f.toLinearMap ∘ₗ (ρ : (a : G) → V →ₗ[A] V) x) (g.toLinearMap ∘ₗ (τ : (a : G) → U →ₗ[A] U) x) =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
rw₂ :
  Eq (α := TensorProduct A V U →ₗ[A] TensorProduct A W P)
    (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x ∘ₗ f.toLinearMap) (g.toLinearMap ∘ₗ (τ : (a : G) → U →ₗ[A] U) x))
    ((σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap)
rw₃ :
  Eq (α := TensorProduct A V U →ₗ[A] TensorProduct A W P)
    (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x ∘ₗ f.toLinearMap) ((π : (a : G) → P →ₗ[A] P) x ∘ₗ g.toLinearMap))
    ((σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap)
⊢ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ
      (ρ.tprod τ : (a : G) → TensorProduct A V U →ₗ[A] TensorProduct A V U) x =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
have rw₄ : Eq (α := TensorProduct A V U →ₗ[A] TensorProduct A W P)
  (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x) ((π : (a : G) → P →ₗ[A] P) x) ∘ₗ
    TensorProduct.map f.toLinearMap g.toLinearMap)
  ((σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
    TensorProduct.map f.toLinearMap g.toLinearMap)
Tactic: rw [tprod_apply, ← TensorProduct.map_comp, f.2, g.2, TensorProduct.map_comp, tprod_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x : G
rw :
  TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ
      TensorProduct.map ((ρ : (a : G) → V →ₗ[A] V) x) ((τ : (a : G) → U →ₗ[A] U) x) =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
rw₁ :
  TensorProduct.map (f.toLinearMap ∘ₗ (ρ : (a : G) → V →ₗ[A] V) x) (g.toLinearMap ∘ₗ (τ : (a : G) → U →ₗ[A] U) x) =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
rw₂ :
  Eq (α := TensorProduct A V U →ₗ[A] TensorProduct A W P)
    (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x ∘ₗ f.toLinearMap) (g.toLinearMap ∘ₗ (τ : (a : G) → U →ₗ[A] U) x))
    ((σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap)
rw₃ :
  Eq (α := TensorProduct A V U →ₗ[A] TensorProduct A W P)
    (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x ∘ₗ f.toLinearMap) ((π : (a : G) → P →ₗ[A] P) x ∘ₗ g.toLinearMap))
    ((σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap)
rw₄ :
  Eq (α := TensorProduct A V U →ₗ[A] TensorProduct A W P)
    (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x) ((π : (a : G) → P →ₗ[A] P) x) ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap)
    ((σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap)
⊢ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ
      (ρ.tprod τ : (a : G) → TensorProduct A V U →ₗ[A] TensorProduct A V U) x =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
have rw₅ : Eq (α := TensorProduct A V U →ₗ[A] TensorProduct A W P)
  (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x) ((π : (a : G) → P →ₗ[A] P) x) ∘ₗ
    TensorProduct.map f.toLinearMap g.toLinearMap)
  (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x) ((π : (a : G) → P →ₗ[A] P) x) ∘ₗ
    TensorProduct.map f.toLinearMap g.toLinearMap)
Tactic: rw [tprod_apply, ← TensorProduct.map_comp, f.2, g.2, TensorProduct.map_comp, tprod_apply]