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
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
g : G
φ : ρ.Equiv σ
⊢ Eq.{u_4 + 1} (α := Module.End A W)
    ((φ.toLinearEquiv.conj : (a : Module.End A V) → Module.End A W) ((ρ : (a : G) → V →ₗ[A] V) g) : Module.End A W)
    ((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W)
have h : ∀ (w : W),
  Eq (α := W)
    ((((φ.toLinearEquiv.conj : (a : Module.End A V) → Module.End A W) ((ρ : (a : G) → V →ₗ[A] V) g) : Module.End A W) :
          (a : W) → W)
        w :
      W)
    ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) w : W)
Tactic: ext w
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (hypothesis)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
g : G
φ : ρ.Equiv σ
w : W
⊢ Eq (α := W)
    ((((φ.toLinearEquiv.conj : (a : Module.End A V) → Module.End A W) ((ρ : (a : G) → V →ₗ[A] V) g) : Module.End A W) :
          (a : W) → W)
        w :
      W)
    ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) w : W)
have this : Eq.{u_3 + 1} (α := V) (((ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑φ.symm : σ.IntertwiningMap ρ).toLinearMap : (a : W) → V) w : V)
  (((↑φ.symm : σ.IntertwiningMap ρ).toLinearMap ∘ₗ (σ : (a : G) → W →ₗ[A] W) g : (a : W) → V) w : V)
Tactic: have := (congr($(φ.symm.toIntertwiningMap.2 g) w)).symm
-- 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
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
g : G
φ : ρ.Equiv σ
w : W
this :
  Eq.{u_3 + 1} (α := V)
    (((ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑φ.symm : σ.IntertwiningMap ρ).toLinearMap : (a : W) → V) w : V)
    (((↑φ.symm : σ.IntertwiningMap ρ).toLinearMap ∘ₗ (σ : (a : G) → W →ₗ[A] W) g : (a : W) → V) w : V)
⊢ Eq (α := W)
    ((((φ.toLinearEquiv.conj : (a : Module.End A V) → Module.End A W) ((ρ : (a : G) → V →ₗ[A] V) g) : Module.End A W) :
          (a : W) → W)
        w :
      W)
    ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) w : W)
have h : Eq.{u_4 + 1} (α := W)
  ((φ : (a : V) → W) ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) ((φ.symm : (a : W) → V) w : V) : V) : W)
  ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) w : W)
Tactic: simp only [LinearMap.coe_comp, coe_toLinearMap, Function.comp_apply, LinearEquiv.conj_apply_apply,
    coe_symm, toLinearEquiv_apply, coe_toIntertwiningMap] at this ⊢
-- 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 σ
v : ρ.asModule
g : G
a : A
⊢ (f.toLinearMap : (a : V) → W) (HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g a) v) =
    HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) (MonoidAlgebra.single g a) : A[G])
      ((f.toLinearMap : (a : V) → W) v : W)
have single : HSMul.hSMul (β := W) a
    ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W)
        ((f : (a : V) → W) ((ρ.asModuleEquiv : (a : ρ.asModule) → V) v : V) : W) :
      W) =
  HSMul.hSMul (β := W) a
    ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W)
        ((σ.asModuleEquiv : (a : σ.asModule) → W) ((f : (a : V) → W) v : W) : W) :
      W)
Tactic: simp [f.isIntertwining]
-- 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 σ
m : A[G]
v : ρ.asModule
⊢ (f.toLinearMap : (a : V) → W) (m • v) =
    HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) m : A[G])
      ((f.toLinearMap : (a : V) → W) v : W)
have zero : (f.toLinearMap : (a : V) → W) (HSMul.hSMul (α := A[G]) 0 v) =
  HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) 0)
    ((f.toLinearMap : (a : V) → W) v : W)
Tactic: induction m using MonoidAlgebra.induction_linear with
          | zero => simp [f.toLinearMap.map_zero]
          | add x y hx hy => simp [add_smul, map_add, hx, hy]
          | single g a => simp [f.isIntertwining]; rfl
Cleared hypotheses: m
-- 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 σ
m : A[G]
v : ρ.asModule
zero :
  (f.toLinearMap : (a : V) → W) (HSMul.hSMul (α := A[G]) 0 v) =
    HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) 0)
      ((f.toLinearMap : (a : V) → W) v : W)
⊢ (f.toLinearMap : (a : V) → W) (m • v) =
    HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) m : A[G])
      ((f.toLinearMap : (a : V) → W) v : W)
have add : ∀ (x y : A[G])
  (hx :
    (f.toLinearMap : (a : V) → W) (x • v) =
      HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) x : A[G])
        ((f.toLinearMap : (a : V) → W) v : W))
  (hy :
    (f.toLinearMap : (a : V) → W) (y • v) =
      HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) y : A[G])
        ((f.toLinearMap : (a : V) → W) v : W)),
  (f.toLinearMap : (a : V) → W) ((x + y) • v) =
    HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) (x + y) : A[G])
      ((f.toLinearMap : (a : V) → W) v : W)
Tactic: induction m using MonoidAlgebra.induction_linear with
          | zero => simp [f.toLinearMap.map_zero]
          | add x y hx hy => simp [add_smul, map_add, hx, hy]
          | single g a => simp [f.isIntertwining]; rfl
Cleared hypotheses: m
-- 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 σ
m : A[G]
v : ρ.asModule
zero :
  (f.toLinearMap : (a : V) → W) (HSMul.hSMul (α := A[G]) 0 v) =
    HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) 0)
      ((f.toLinearMap : (a : V) → W) v : W)
add :
  ∀ (x y : A[G])
    (hx :
      (f.toLinearMap : (a : V) → W) (x • v) =
        HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) x : A[G])
          ((f.toLinearMap : (a : V) → W) v : W))
    (hy :
      (f.toLinearMap : (a : V) → W) (y • v) =
        HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) y : A[G])
          ((f.toLinearMap : (a : V) → W) v : W)),
    (f.toLinearMap : (a : V) → W) ((x + y) • v) =
      HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) (x + y) : A[G])
        ((f.toLinearMap : (a : V) → W) v : W)
⊢ (f.toLinearMap : (a : V) → W) (m • v) =
    HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) m : A[G])
      ((f.toLinearMap : (a : V) → W) v : W)
have single : ∀ (g : G) (a : A),
  (f.toLinearMap : (a : V) → W) (HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g a) v) =
    HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) (MonoidAlgebra.single g a) : A[G])
      ((f.toLinearMap : (a : V) → W) v : W)
Tactic: induction m using MonoidAlgebra.induction_linear with
          | zero => simp [f.toLinearMap.map_zero]
          | add x y hx hy => simp [add_smul, map_add, hx, hy]
          | single g a => simp [f.isIntertwining]; rfl
Cleared hypotheses: m
-- 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 : V →ₗ[A] W
g₁ g₂ : ρ.IntertwiningMap σ
⊢ { toFun := (⇑(g₁ + g₂).toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule)
      { toFun := (⇑g₁.toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ :
        LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule }
      { toFun := (⇑g₂.toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ :
        LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule }
have h : ∀ (x : ρ.asModule),
  Eq.{u_4 + 1} (α := σ.asModule)
    ((({ toFun := (⇑(g₁ + g₂).toLinearMap : (a : V) → W), map_add' := sorry, map_smul' := sorry } :
            LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule) :
          (a : ρ.asModule) → σ.asModule)
        x :
      σ.asModule)
    ((HAdd.hAdd (α := LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule)
            { toFun := (⇑g₁.toLinearMap : (a : V) → W), map_add' := sorry, map_smul' := sorry :
              LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule }
            { toFun := (⇑g₂.toLinearMap : (a : V) → W), map_add' := sorry, map_smul' := sorry :
              LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule } :
          (a : ρ.asModule) → σ.asModule)
        x :
      σ.asModule)
Tactic: ext
-- 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 : V →ₗ[A] W
t : A
g : ρ.IntertwiningMap σ
⊢ { toFun := (⇑(t • g).toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := A) (β := LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule)
      ((RingHom.id A : (a : A) → A) t : A)
      { toFun := (⇑g.toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ :
        LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule }
have h : ∀ (x : ρ.asModule),
  Eq.{u_4 + 1} (α := σ.asModule)
    ((({ toFun := (⇑(t • g).toLinearMap : (a : V) → W), map_add' := sorry, map_smul' := sorry } :
            LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule) :
          (a : ρ.asModule) → σ.asModule)
        x :
      σ.asModule)
    ((HSMul.hSMul (α := A) (β := LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule)
            ((RingHom.id A : (a : A) → A) t : A)
            { toFun := (⇑g.toLinearMap : (a : V) → W), map_add' := sorry, map_smul' := sorry :
              LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule } :
          (a : ρ.asModule) → σ.asModule)
        x :
      σ.asModule)
Tactic: ext
-- 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 : LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule
g : G
⊢ Eq (α := V →ₗ[A] W) ({ toAddHom := f.toAddHom, map_smul' := ⋯ } ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g)
    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ { toAddHom := f.toAddHom, map_smul' := ⋯ })
have h : ∀ (v : V),
  Eq.{u_4 + 1} (α := W)
    (({ toAddHom := f.toAddHom, map_smul' := sorry } ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g : (a : V) → W) v : W)
    (((σ : (a : G) → W →ₗ[A] W) g ∘ₗ { toAddHom := f.toAddHom, map_smul' := sorry } : (a : V) → W) v : W)
Tactic: ext v
-- 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 τ
x x_1 : ρ.IntertwiningMap σ
⊢ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x + x_1).toLinearMap) ⋯ =
    LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x.toLinearMap) ⋯ +
      LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x_1.toLinearMap) ⋯
have h : ∀ (x_2 : V),
  Eq.{u_5 + 1} (α := U)
    (((LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x + x_1).toLinearMap) sorry).toLinearMap :
          (a : V) → U)
        x_2 :
      U)
    (((LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x.toLinearMap) sorry +
              LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x_1.toLinearMap) sorry).toLinearMap :
          (a : V) → U)
        x_2 :
      U)
Tactic: ext
-- 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 τ
x : A
x_1 : ρ.IntertwiningMap σ
⊢ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x • x_1).toLinearMap) ⋯ =
    HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) x : A)
      (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x_1.toLinearMap) ⋯)
have h : ∀ (x_2 : V),
  Eq.{u_5 + 1} (α := U)
    (((LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x • x_1).toLinearMap) sorry).toLinearMap :
          (a : V) → U)
        x_2 :
      U)
    (((HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) x : A)
              (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x_1.toLinearMap) sorry)).toLinearMap :
          (a : V) → U)
        x_2 :
      U)
Tactic: ext
-- 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 : V →ₗ[A] W
x x_1 : σ.IntertwiningMap τ
⊢ {
      toFun := fun (g : ρ.IntertwiningMap σ) ↦
        LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x + x_1).toLinearMap ∘ₗ g.toLinearMap) ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ)
      {
        toFun := fun (g : ρ.IntertwiningMap σ) ↦
          LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x.toLinearMap ∘ₗ g.toLinearMap) ⋯,
        map_add' := ⋯, map_smul' := ⋯ : ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ }
      {
        toFun := fun (g : ρ.IntertwiningMap σ) ↦
          LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x_1.toLinearMap ∘ₗ g.toLinearMap) ⋯,
        map_add' := ⋯, map_smul' := ⋯ : ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ }
have h : ∀ (x_2 : ρ.IntertwiningMap σ) (x_3 : V),
  Eq.{u_5 + 1} (α := U)
    ((toLinearMap.{u_1, u_2, u_3, u_5} (G := G) (ρ := ρ) (σ := τ)
            (({
                  toFun := fun (g : ρ.IntertwiningMap σ) ↦
                    LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x + x_1).toLinearMap ∘ₗ g.toLinearMap) sorry,
                  map_add' := sorry, map_smul' := sorry } :
                (a : ρ.IntertwiningMap σ) → ρ.IntertwiningMap τ)
              x_2) :
          (a : V) → U)
        x_3 :
      U)
    ((toLinearMap.{u_1, u_2, u_3, u_5} (G := G) (ρ := ρ) (σ := τ)
            ((HAdd.hAdd (α := ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ)
                  {
                    toFun := fun (g : ρ.IntertwiningMap σ) ↦
                      LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x.toLinearMap ∘ₗ g.toLinearMap) sorry,
                    map_add' := sorry, map_smul' := sorry : ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ }
                  {
                    toFun := fun (g : ρ.IntertwiningMap σ) ↦
                      LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x_1.toLinearMap ∘ₗ g.toLinearMap) sorry,
                    map_add' := sorry, map_smul' := sorry : ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ } :
                (a : ρ.IntertwiningMap σ) → ρ.IntertwiningMap τ)
              x_2) :
          (a : V) → U)
        x_3 :
      U)
Tactic: ext
-- 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 : V →ₗ[A] W
x : A
x_1 : σ.IntertwiningMap τ
⊢ {
      toFun := fun (g : ρ.IntertwiningMap σ) ↦
        LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x • x_1).toLinearMap ∘ₗ g.toLinearMap) ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := A) (β := ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ) ((RingHom.id A : (a : A) → A) x : A)
      {
        toFun := fun (g : ρ.IntertwiningMap σ) ↦
          LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x_1.toLinearMap ∘ₗ g.toLinearMap) ⋯,
        map_add' := ⋯, map_smul' := ⋯ : ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ }
have h : ∀ (x_2 : ρ.IntertwiningMap σ) (x_3 : V),
  Eq.{u_5 + 1} (α := U)
    ((toLinearMap.{u_1, u_2, u_3, u_5} (G := G) (ρ := ρ) (σ := τ)
            (({
                  toFun := fun (g : ρ.IntertwiningMap σ) ↦
                    LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x • x_1).toLinearMap ∘ₗ g.toLinearMap) sorry,
                  map_add' := sorry, map_smul' := sorry } :
                (a : ρ.IntertwiningMap σ) → ρ.IntertwiningMap τ)
              x_2) :
          (a : V) → U)
        x_3 :
      U)
    ((toLinearMap.{u_1, u_2, u_3, u_5} (G := G) (ρ := ρ) (σ := τ)
            ((HSMul.hSMul (α := A) (β := ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ)
                  ((RingHom.id A : (a : A) → A) x : A)
                  {
                    toFun := fun (g : ρ.IntertwiningMap σ) ↦
                      LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x_1.toLinearMap ∘ₗ g.toLinearMap) sorry,
                    map_add' := sorry, map_smul' := sorry : ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ } :
                (a : ρ.IntertwiningMap σ) → ρ.IntertwiningMap τ)
              x_2) :
          (a : V) → U)
        x_3 :
      U)
Tactic: ext
-- 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 : ℕ
⊢ (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (f ^ n) =
    HPow.hPow (α := V →ₗ[A] V) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) n
have zero : (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (HPow.hPow (β := ℕ) f 0) =
  HPow.hPow (α := V →ₗ[A] V) (β := ℕ) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) 0
Tactic: induction n with
      | zero => rfl
      | succ n ih => simp only [pow_succ, coe_mul, show f ^ (n + 1) = f ^ n * f from rfl, ih]
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
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 only [pow_succ, coe_mul, show f ^ (n + 1) = f ^ n * f from rfl, ih]
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
f : ρ.IntertwiningMap ρ
n : ℕ
⊢ (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (f ^ n) =
    HPow.hPow (α := V →ₗ[A] V) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) n
have zero : (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (HPow.hPow (β := ℕ) f 0) =
  HPow.hPow (α := V →ₗ[A] V) (β := ℕ) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) 0
Tactic: induction n with
      | zero => rfl
      | succ n ih => simp [ih, pow_succ]
Cleared hypotheses: n