awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Induced
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 : (↑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:
simp [coinvariantsTensorIndInv, coinvariantsTensorMk, coinvariantsTensorIndHom]

Premises used: Rep.coinvariantsTensorIndInv, Rep.coinvariantsTensorMk, Rep.coinvariantsTensorIndHom
-- Module: Mathlib.RepresentationTheory.Intertwining
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
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)
⊢ f ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ f

Tactic:
ext v
-- Module: Mathlib.RepresentationTheory.Intertwining
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
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:
hf g v
-- Module: Mathlib.RepresentationTheory.Intertwining
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
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:
exact hf g v
-- Module: Mathlib.RepresentationTheory.Intertwining
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)
rw₂ 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

Tactic:
rw [← LinearMap.comp_assoc, f.2, LinearMap.comp_assoc]

Premises used: LinearMap.comp_assoc, Representation.IntertwiningMap.isIntertwining'
-- Module: Mathlib.RepresentationTheory.Intertwining
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
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
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.RepresentationTheory.Intertwining
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
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 }
⊢ { toLinearMap := toLinearMap, isIntertwining' := isIntertwining' : ρ.IntertwiningMap σ } = g

Tactic:
cases g
-- Module: Mathlib.RepresentationTheory.Intertwining
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
toLinearMap : V →ₗ[A] W
isIntertwining' : ∀ (g : G), toLinearMap ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ toLinearMap
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:
simpa using h
-- Module: Mathlib.RepresentationTheory.Intertwining
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
⊢ Function.Injective (β := V →ₗ[A] W) fun (f : ρ.IntertwiningMap σ) ↦ f.toLinearMap

Tactic:
fun _ _ ↦ ext

Premises used: Representation.IntertwiningMap.ext, Function.Injective
-- Module: Mathlib.RepresentationTheory.Intertwining
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)
h₁ : ∀ (x : V), Eq.{u_4 + 1} (α := W) ((f.toLinearMap : (a : V) → W) x : W) ((g.toLinearMap : (a : V) → W) x : W)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.RepresentationTheory.Intertwining
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)
x : V
⊢ Eq.{u_4 + 1} (α := W) ((f.toLinearMap : (a : V) → W) x : W) ((g.toLinearMap : (a : V) → W) x : W)

Tactic:
congrFun h x

Premises used: congrFun
-- Module: Mathlib.RepresentationTheory.Intertwining
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)
x : V
⊢ Eq.{u_4 + 1} (α := W) ((f.toLinearMap : (a : V) → W) x : W) ((g.toLinearMap : (a : V) → W) x : W)

Tactic:
exact congrFun h x

Premises used: congrFun
-- Module: Mathlib.RepresentationTheory.Intertwining
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 : ρ.IntertwiningMap σ
⊢ (↑f :
      [inst_6 : FunLike (ρ.IntertwiningMap σ) V W] →
        [SemilinearMapClass (ρ.IntertwiningMap σ) (RingHom.id A) V W] → V →ₗ[A] W) =
    f.toLinearMap

Tactic:
rfl

Premises used: SemilinearMapClass.semilinearMap, rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
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 : V →ₗ[A] W
h : ∀ (g : G), f ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ f
⊢ Eq (α := (a : V) → W) (⇑{ toLinearMap := f, isIntertwining' := h : ρ.IntertwiningMap σ } : (a : V) → W)
    (⇑f : (a : V) → W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
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 : V →ₗ[A] W
h : ∀ (g : G), f ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ f
⊢ { toLinearMap := f, isIntertwining' := h : ρ.IntertwiningMap σ }.toLinearMap = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
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 : ρ.IntertwiningMap σ
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)

Tactic:
congr($(f.isIntertwining' g) v)

Premises used: congrArg, id, Representation.IntertwiningMap.isIntertwining', DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Intertwining
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 : ρ.IntertwiningMap σ
v : V
⊢ Eq.{u_4 + 1} (α := W) ((f.toLinearMap : (a : V) → W) v : W) ((f : (a : V) → W) v : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
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 : ρ.IntertwiningMap σ
⊢ Eq (α := (a : V) → W) (⇑f.toLinearMap : (a : V) → W) (⇑f : (a : V) → W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
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 : 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)
v : V
⊢ Eq.{u_4 + 1} (α := W) ((LinearMap.intertwiningMap_of_isIntertwiningMap ρ σ f hf : (a : V) → W) v : W)
    ((f : (a : V) → W) v : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
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
⊢ ∀ (g : G), Eq (α := V →ₗ[A] W) (0 ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g) ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ 0)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
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
⊢ Eq (α := (a : V) → W) (⇑0 : (a : V) → W) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
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
⊢ Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
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 g : ρ.IntertwiningMap σ
⊢ ∀ (g_1 : G),
    (f.toLinearMap + g.toLinearMap) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g_1 =
      (σ : (a : G) → W →ₗ[A] W) g_1 ∘ₗ (f.toLinearMap + g.toLinearMap)

Tactic:
simp [LinearMap.add_comp, LinearMap.comp_add, f.2, g.2,]

Premises used: LinearMap.add_comp, Representation.IntertwiningMap.isIntertwining', LinearMap.comp_add
-- Module: Mathlib.RepresentationTheory.Intertwining
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 σ
⊢ (⇑(f + g) : (a : V) → W) = HAdd.hAdd (α := (a : V) → W) (⇑f : (a : V) → W) (⇑g : (a : V) → W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
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 σ
⊢ (f + g).toLinearMap = f.toLinearMap + g.toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
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
n : ℕ
f : ρ.IntertwiningMap σ
⊢ ∀ (g : G), (n • f.toLinearMap) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ (n • f.toLinearMap)

Tactic:
simp [LinearMap.smul_comp, LinearMap.comp_smul, f.2]

Premises used: LinearMap.smul_comp, Representation.IntertwiningMap.isIntertwining', LinearMap.comp_smul
-- Module: Mathlib.RepresentationTheory.Intertwining
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 : ρ.IntertwiningMap σ
n : ℕ
⊢ (⇑(n • f) : (a : V) → W) = HSMul.hSMul (β := (a : V) → W) n (⇑f : (a : V) → W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
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 : ℕ
rw rw₁ : HSMul.hSMul (β := (a : V) → W) n (⇑f : (a : V) → W) = HSMul.hSMul (β := (a : V) → W) n (⇑f : (a : V) → W)
⊢ (⇑(n • f) : (a : V) → W) = HSMul.hSMul (β := (a : V) → W) n (⇑f : (a : V) → W)

Tactic:
rw [coe_nsmul]

Premises used: Representation.IntertwiningMap.coe_nsmul
-- Module: Mathlib.RepresentationTheory.Intertwining
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 σ
g : G
w : W
h : w ∈ f.range
v : V
hv : (f.toLinearMap : (a : V) → W) v = w
⊢ Eq.{u_4 + 1} (α := W)
    ((f.toLinearMap : (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) w : W)

Tactic:
simp [f.isIntertwining, (f.toLinearMap_apply _ _ _).symm.trans hv]

Premises used: Representation.IntertwiningMap.toLinearMap_apply, Representation.IntertwiningMap.isIntertwining, Eq.symm, Eq.trans
-- Module: Mathlib.RepresentationTheory.Intertwining
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 : ρ.IntertwiningMap σ
w : W
⊢ w ∈ range ρ σ f ↔ ∃ (v : V), (f : (a : V) → W) v = w

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.RepresentationTheory.Intertwining
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 σ
g : G
⊢ ∀ ⦃v : V⦄, v ∈ f.ker → Membership.mem (α := V) f.ker ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V)

Tactic:
simp +contextual [f.isIntertwining]

Premises used: Representation.IntertwiningMap.isIntertwining
-- Module: Mathlib.RepresentationTheory.Intertwining
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 : ρ.IntertwiningMap σ
v : V
⊢ v ∈ ker ρ σ f ↔ Eq.{u_4 + 1} (α := W) ((f : (a : V) → W) v : W) (0 : W)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.RepresentationTheory.Intertwining
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
f : ι → ρ.IntertwiningMap σ
⊢ Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ ∅, f i))
    (∑ i ∈ ∅, (f i).toLinearMap)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
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
f : ι → ρ.IntertwiningMap σ
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:
simp [Finset.sum_insert hi, ih]

Premises used: Finset.sum_insert
-- Module: Mathlib.RepresentationTheory.Intertwining
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)
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.insert i s, f i))
      (∑ i ∈ Insert.insert i s, (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)

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih => simp [Finset.sum_insert hi, ih]

Premises used: Insert.insert