awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
Goal:
k : Type u
G : Type v
H : Type v'
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A_1 : Rep.{w, u, v} k G
B_1 : Rep k H
A : Rep k G
B : Rep k H
f : A ⟶ res φ B
g : G
⊢ Eq (α := TensorProduct k (H →₀ k) (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
    (TensorProduct.lift
      (LinearMap.compl₂ (R₂ := k) (N := (↑A : Type (max (max u v') w))) (σ₂₃ := RingHom.id k) (σ₄₂ := RingHom.id k)
        (((lift ((↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) k H :
              (a : H → (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) →
                (H →₀ k) →ₗ[k] (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
            fun (h : H) ↦
            (B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) h⁻¹ ∘ₗ
              (Hom.hom f).toLinearMap) ∘ₗ
          (Representation.leftRegular k H : (a : H) → (H →₀ k) →ₗ[k] H →₀ k) ((φ : (a : G) → H) g))
        ((A.ρ : (a : G) → (↑A : Type (max (max u v') w)) →ₗ[k] (↑A : Type (max (max u v') w))) g)))
    (TensorProduct.lift
      ((lift ((↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) k H :
          (a : H → (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) →
            (H →₀ k) →ₗ[k] (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
        fun (h : H) ↦
        (B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) h⁻¹ ∘ₗ
          (Hom.hom f).toLinearMap))
have e_f' : Eq (α := (H →₀ k) →ₗ[k] (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
  (LinearMap.compl₂ (R₂ := k) (N := (↑A : Type (max (max u v') w))) (σ₂₃ := RingHom.id k) (σ₄₂ := RingHom.id k)
    (((lift ((↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) k H :
          (a : H → (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) →
            (H →₀ k) →ₗ[k] (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
        fun (h : H) ↦
        (B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) h⁻¹ ∘ₗ
          (Hom.hom f).toLinearMap) ∘ₗ
      (Representation.leftRegular k H : (a : H) → (H →₀ k) →ₗ[k] H →₀ k) ((φ : (a : G) → H) g))
    ((A.ρ : (a : G) → (↑A : Type (max (max u v') w)) →ₗ[k] (↑A : Type (max (max u v') w))) g))
  ((lift ((↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) k H :
      (a : H → (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) →
        (H →₀ k) →ₗ[k] (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
    fun (h : H) ↦
    (B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) h⁻¹ ∘ₗ
      (Hom.hom f).toLinearMap)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
Goal:
k : Type u
G : Type v
H : Type v'
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A_1 : Rep.{w, u, v} k G
B_1 : Rep k H
A : Rep k G
B : Rep k H
f : A ⟶ res φ B
g : H
⊢ Eq (α := IndV φ A.ρ →ₗ[k] (↑B : Type (max (max u v') w)))
    (Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
        (TensorProduct.lift
          ((lift ((↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) k H :
              (a : H → (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) →
                (H →₀ k) →ₗ[k] (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
            fun (h : H) ↦
            (B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) h⁻¹ ∘ₗ
              (Hom.hom f).toLinearMap))
        ⋯ ∘ₗ
      (Representation.ind φ A.ρ : (a : H) → IndV φ A.ρ →ₗ[k] IndV φ A.ρ) g)
    ((B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) g ∘ₗ
      Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
        (TensorProduct.lift
          ((lift ((↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) k H :
              (a : H → (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) →
                (H →₀ k) →ₗ[k] (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
            fun (h : H) ↦
            (B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) h⁻¹ ∘ₗ
              (Hom.hom f).toLinearMap))
        ⋯)
have H₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
Goal:
k : Type u
G_1 : Type v
H_1 : Type v'
inst : CommRing k
inst_1 : Group G_1
inst_2 : Group H_1
φ_1 : G_1 →* H_1
A_1 : Rep.{w, u, v} k G_1
G H : Type u
inst_3 : Group G
inst_4 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
x : H
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
Goal:
k : Type u
G_1 : Type v
H_1 : Type v'
inst : CommRing k
inst_1 : Group G_1
inst_2 : Group H_1
φ_1 : G_1 →* H_1
A_1 : Rep.{w, u, v} k G_1
G H : Type u
inst_3 : Group G
inst_4 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
s : G
⊢ TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
      ((Functor.obj (Functor.obj (MonoidalCategory.curriedTensor (Rep k G)) A) (res φ B)).ρ :
          (a : G) →
            (↑(((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)) : Type u) →ₗ[k]
              (↑(((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)) : Type u))
        s =
    TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1)
have simp : TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
    TensorProduct.map ((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) s)
      ((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) ((φ : (a : G) → H) s)) =
  TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1)
Tactic: simp only [MonoidalCategory.curriedTensor_obj_obj, tensor_V, tensor_ρ, tprod_apply,
      MonoidHom.coe_comp, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
Goal:
k : Type u
G_1 : Type v
H_1 : Type v'
inst : CommRing k
inst_1 : Group G_1
inst_2 : Group H_1
φ_1 : G_1 →* H_1
A_1 : Rep.{w, u, v} k G_1
G H : Type u
inst_3 : Group G
inst_4 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
s : G
⊢ TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
      TensorProduct.map ((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) s)
        ((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) ((φ : (a : G) → H) s)) =
    TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1)
have a : ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
  Eq (α := ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
    (((((TensorProduct.AlgebraTensorModule.curry
                    (TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
                      TensorProduct.map ((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) s)
                        ((B.ρ : (a : H) → (↑B : Type u) →ₗ[k] (↑B : Type u)) ((φ : (a : G) → H) s))) :
                  (↑A : Type u) →ₗ[k] (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants) :
                (a : (↑A : Type u)) → (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
              x :
            (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants) :
          (a : (↑B : Type u)) → ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
        y :
      ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
    (((((TensorProduct.AlgebraTensorModule.curry
                    (TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1)) :
                  (↑A : Type u) →ₗ[k] (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants) :
                (a : (↑A : Type u)) → (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
              x :
            (↑B : Type u) →ₗ[k] ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants) :
          (a : (↑B : Type u)) → ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
        y :
      ((Representation.ind φ A.ρ).tprod B.ρ).Coinvariants)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
Goal:
k : Type u
G_1 : Type v
H_1 : Type v'
inst : CommRing k
inst_1 : Group G_1
inst_2 : Group H_1
φ_1 : G_1 →* H_1
A_1 : Rep.{w, u, v} k G_1
G H : Type u
inst_3 : Group G
inst_4 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
⊢ coinvariantsTensorIndHom φ A B ≫ coinvariantsTensorIndInv φ A B =
    𝟙 ((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B)
have hfg : ∀ (h : H) (a : (↑A : Type u)) (b : (↑B : Type u)),
  Eq (α := (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u))
    ((((((TensorProduct.AlgebraTensorModule.curry
                          (((ind φ A).coinvariantsTensorMk B).compr₂
                              (ModuleCat.Hom.hom (coinvariantsTensorIndHom φ A B ≫ coinvariantsTensorIndInv φ A B)) ∘ₗ
                            Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
                        lsingle h :
                      k →ₗ[k]
                        (↑A : Type u) →ₗ[k]
                          (↑B : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u)) :
                    (a : k) →
                      (↑A : Type u) →ₗ[k]
                        (↑B : Type u) →ₗ[k] (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
                  1 :
                (a : (↑A : Type u)) → (↑B : Type u) →ₗ[k] (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
              a :
            (↑B : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u)) :
          (a : (↑B : Type u)) → (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
        b :
      (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u))
    ((((((TensorProduct.AlgebraTensorModule.curry
                          (((ind φ A).coinvariantsTensorMk B).compr₂
                              (ModuleCat.Hom.hom (𝟙 ((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B))) ∘ₗ
                            Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
                        lsingle h :
                      k →ₗ[k]
                        (↑A : Type u) →ₗ[k]
                          (↑B : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u)) :
                    (a : k) →
                      (↑A : Type u) →ₗ[k]
                        (↑B : Type u) →ₗ[k] (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
                  1 :
                (a : (↑A : Type u)) → (↑B : Type u) →ₗ[k] (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
              a :
            (↑B : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u)) :
          (a : (↑B : Type u)) → (↑(((coinvariantsTensor k H).obj (ind φ A)).obj B) : Type u))
        b :
      (↑((Functor.obj (coinvariantsTensor k H) (ind φ A)).obj B) : Type u))
Tactic: ext h a b
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
Goal:
k : Type u
G_1 : Type v
H_1 : Type v'
inst : CommRing k
inst_1 : Group G_1
inst_2 : Group H_1
φ_1 : G_1 →* H_1
A_1 : Rep.{w, u, v} k G_1
G H : Type u
inst_3 : Group G
inst_4 : Group H
φ : G →* H
A : Rep k G
B : Rep k H
⊢ coinvariantsTensorIndInv φ A B ≫ coinvariantsTensorIndHom φ A B =
    𝟙 ((Functor.obj (coinvariantsTensor k G) A).obj (res φ B))
have hfg : ∀ (x : (↑A : Type u)) (x_1 : (↑(res φ B) : Type u)),
  Eq (α := (↑((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)) : Type u))
    ((((LinearMap.compr₂ (A.coinvariantsTensorMk (res φ B))
                  (ModuleCat.Hom.hom (coinvariantsTensorIndInv φ A B ≫ coinvariantsTensorIndHom φ A B)) :
                (a : (↑A : Type u)) →
                  (↑(res φ B) : Type u) →ₗ[k] (↑(((coinvariantsTensor k G).obj A).obj (res φ B)) : Type u))
              x :
            (↑(res φ B) : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)) : Type u)) :
          (a : (↑(res φ B) : Type u)) → (↑(((coinvariantsTensor k G).obj A).obj (res φ B)) : Type u))
        x_1 :
      (↑((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)) : Type u))
    ((((LinearMap.compr₂ (A.coinvariantsTensorMk (res φ B))
                  (ModuleCat.Hom.hom (𝟙 ((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)))) :
                (a : (↑A : Type u)) →
                  (↑(res φ B) : Type u) →ₗ[k] (↑(((coinvariantsTensor k G).obj A).obj (res φ B)) : Type u))
              x :
            (↑(res φ B) : Type u) →ₗ[k] (↑((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)) : Type u)) :
          (a : (↑(res φ B) : Type u)) → (↑(((coinvariantsTensor k G).obj A).obj (res φ B)) : Type u))
        x_1 :
      (↑((Functor.obj (coinvariantsTensor k G) A).obj (res φ B)) : Type 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 : Semiring 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
hf :
  ∀ (g : G) (v : V),
    Eq (α := W) ((f : (a : V) → W) ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) : W)
      ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) ((f : (a : V) → W) v : W) : W)
g : G
⊢ f ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ f
have h : ∀ (v : V),
  Eq.{u_4 + 1} (α := W) ((f ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g : (a : V) → W) v : W)
    (((σ : (a : G) → W →ₗ[A] W) g ∘ₗ f : (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 : Semiring 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
f : ρ.IntertwiningMap σ
g : G
l : U →ₗ[A] V
⊢ f.toLinearMap ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ l = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ f.toLinearMap ∘ₗ l
have rw : (f.toLinearMap ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g) ∘ₗ l = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ f.toLinearMap ∘ₗ l
Tactic: rw [← LinearMap.comp_assoc, f.2, LinearMap.comp_assoc]
-- 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 : Semiring 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
f : ρ.IntertwiningMap σ
g : G
l : U →ₗ[A] V
rw : (f.toLinearMap ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g) ∘ₗ l = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ f.toLinearMap ∘ₗ l
⊢ f.toLinearMap ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ l = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ f.toLinearMap ∘ₗ l
have rw₁ : Eq (α := U →ₗ[A] W) (((σ : (a : G) → W →ₗ[A] W) g ∘ₗ f.toLinearMap) ∘ₗ l)
  ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ f.toLinearMap ∘ₗ l)
Tactic: rw [← LinearMap.comp_assoc, f.2, LinearMap.comp_assoc]
-- 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 : Semiring 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
f : ρ.IntertwiningMap σ
g : G
l : U →ₗ[A] V
rw : (f.toLinearMap ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g) ∘ₗ l = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ f.toLinearMap ∘ₗ l
rw₁ :
  Eq (α := U →ₗ[A] W) (((σ : (a : G) → W →ₗ[A] W) g ∘ₗ f.toLinearMap) ∘ₗ l)
    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ f.toLinearMap ∘ₗ l)
⊢ f.toLinearMap ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ l = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ f.toLinearMap ∘ₗ l
have rw₂ : Eq (α := U →ₗ[A] W) ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ f.toLinearMap ∘ₗ l)
  ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ f.toLinearMap ∘ₗ l)
Tactic: rw [← LinearMap.comp_assoc, f.2, LinearMap.comp_assoc]
-- 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 : Semiring 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
f g : ρ.IntertwiningMap σ
h : f.toLinearMap = g.toLinearMap
⊢ f = g
have mk : ∀ (toLinearMap : V →ₗ[A] W)
  (isIntertwining' : ∀ (g : G), toLinearMap ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ toLinearMap)
  (h :
    { toLinearMap := toLinearMap, isIntertwining' := isIntertwining' : ρ.IntertwiningMap σ }.toLinearMap =
      g.toLinearMap),
  { toLinearMap := toLinearMap, isIntertwining' := isIntertwining' : ρ.IntertwiningMap σ } = g
Tactic: cases f
Cleared hypotheses: f, h
-- 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 : Semiring 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 : ρ.IntertwiningMap σ
toLinearMap : V →ₗ[A] W
isIntertwining' : ∀ (g : G), toLinearMap ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ toLinearMap
h : { toLinearMap := toLinearMap, isIntertwining' := isIntertwining' : ρ.IntertwiningMap σ }.toLinearMap = g.toLinearMap
⊢ { toLinearMap := toLinearMap, isIntertwining' := isIntertwining' : ρ.IntertwiningMap σ } = g
have mk : ∀ (toLinearMap_1 : V →ₗ[A] W)
  (isIntertwining'_1 :
    ∀ (g : G), toLinearMap_1 ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ toLinearMap_1)
  (h :
    { toLinearMap := toLinearMap, isIntertwining' := isIntertwining' : ρ.IntertwiningMap σ }.toLinearMap =
      { toLinearMap := toLinearMap_1, isIntertwining' := isIntertwining'_1 : ρ.IntertwiningMap σ }.toLinearMap),
  { toLinearMap := toLinearMap, isIntertwining' := isIntertwining' : ρ.IntertwiningMap σ } =
    { toLinearMap := toLinearMap_1, isIntertwining' := isIntertwining'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- 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 : Semiring 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
f g : ρ.IntertwiningMap σ
h : Eq (α := V → W) ((fun (f : ρ.IntertwiningMap σ) ↦ f.toFun) f) ((fun (f : ρ.IntertwiningMap σ) ↦ f.toFun) g)
⊢ f = g
have h₁ : ∀ (x : V), Eq.{u_4 + 1} (α := W) ((f.toLinearMap : (a : V) → W) x : W) ((g.toLinearMap : (a : V) → W) x : W)
Tactic: ext x
-- 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 : Semiring 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 : ℕ
⊢ (⇑(n • f) : (a : V) → W) = HSMul.hSMul (β := (a : V) → W) n (⇑f : (a : V) → W)
have rw : HSMul.hSMul (β := (a : V) → W) n (⇑f : (a : V) → W) = HSMul.hSMul (β := (a : V) → W) n (⇑f : (a : V) → W)
Tactic: rw [coe_nsmul]
-- 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 : Semiring 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
ι : Type u_6
s : Finset ι
f : ι → ρ.IntertwiningMap σ
⊢ Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ s, f i))
    (∑ i ∈ s, (f i).toLinearMap)
have empty : Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ ∅, f i))
  (∑ i ∈ ∅, (f i).toLinearMap)
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih => simp [Finset.sum_insert hi, ih]
Cleared hypotheses: s
-- 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 : Semiring 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
ι : Type u_6
s : Finset ι
f : ι → ρ.IntertwiningMap σ
empty :
  Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ ∅, f i))
    (∑ i ∈ ∅, (f i).toLinearMap)
⊢ Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ s, f i))
    (∑ i ∈ s, (f i).toLinearMap)
have insert : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
  (ih :
    Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ s, f i))
      (∑ i ∈ s, (f i).toLinearMap)),
  Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ insert i s, f i))
    (∑ i ∈ insert i s, (f i).toLinearMap)
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih => simp [Finset.sum_insert hi, ih]
Cleared hypotheses: s
-- 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 : Semiring 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
ι : Type u_6
s : Finset ι
f : ι → ρ.IntertwiningMap σ
⊢ Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ s, f i))
    (∑ i ∈ s, (f i).toLinearMap)
have empty : Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ ∅, f i))
  (∑ i ∈ ∅, (f i).toLinearMap)
Tactic: classical induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih => simp [Finset.sum_insert hi, ih]
Cleared hypotheses: s
-- 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 : Semiring 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
ι : Type u_6
s : Finset ι
f : ι → ρ.IntertwiningMap σ
empty :
  Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ ∅, f i))
    (∑ i ∈ ∅, (f i).toLinearMap)
⊢ Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ s, f i))
    (∑ i ∈ s, (f i).toLinearMap)
have insert : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
  (ih :
    Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ s, f i))
      (∑ i ∈ s, (f i).toLinearMap)),
  Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ insert i s, f i))
    (∑ i ∈ insert i s, (f i).toLinearMap)
Tactic: classical induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih => simp [Finset.sum_insert hi, ih]
Cleared hypotheses: s