awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
e : ρ.Equiv σ
x : X
⊢ Eq (α := (↑(of σ) : Type w))
    ((Hom.hom (mkIso e).hom : (a : (↑(of ρ) : Type w)) → (↑(of σ) : Type w)) x : (↑(of σ) : Type w))
    (((↑e : ρ.IntertwiningMap σ).toLinearMap : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
e : ρ.Equiv σ
⊢ (Hom.hom (mkIso e).hom).toLinearMap = (↑e : ρ.IntertwiningMap σ).toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
e : ρ.Equiv σ
⊢ (Hom.hom (mkIso e).inv).toLinearMap = (↑e.symm : σ.IntertwiningMap ρ).toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
e : ρ.Equiv σ
y : Y
⊢ Eq (α := (↑(of ρ) : Type w))
    ((Hom.hom (mkIso e).inv : (a : (↑(of σ) : Type w)) → (↑(of ρ) : Type w)) y : (↑(of ρ) : Type w))
    ((e.symm : (a : Y) → X) y : X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
e : ρ.Equiv σ
⊢ Hom.hom (mkIso e).hom = (↑e : ρ.IntertwiningMap σ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
A B C : Rep.{w, u, v} k G
Z : Type w
inst_6 : AddCommGroup Z
inst_7 : Module k Z
τ : Representation k G Z
i : A ≅ B
x : (↑A : Type w)
⊢ (ConcreteCategory.hom (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) i.inv :
        (a : (↑B : Type w)) → (↑A : Type w))
      ((ConcreteCategory.hom (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) i.hom :
            (a : (↑A : Type w)) → (↑B : Type w))
          x :
        (↑B : Type w)) =
    x

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
A B C : Rep.{w, u, v} k G
Z : Type w
inst_6 : AddCommGroup Z
inst_7 : Module k Z
τ : Representation k G Z
i : A ≅ B
x : (↑B : Type w)
⊢ (ConcreteCategory.hom (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) i.hom :
        (a : (↑A : Type w)) → (↑B : Type w))
      ((ConcreteCategory.hom (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) i.inv :
            (a : (↑B : Type w)) → (↑A : Type w))
          x :
        (↑A : Type w)) =
    x

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X_1 Y_1 : Type w
inst_2 : AddCommGroup X_1
inst_3 : AddCommGroup Y_1
inst_4 : Module k X_1
inst_5 : Module k Y_1
ρ : Representation k G X_1
σ : Representation k G Y_1
A B C : Rep.{w, u, v} k G
Z : Type w
inst_6 : AddCommGroup Z
inst_7 : Module k Z
τ : Representation k G Z
X Y : Rep.{w, u, v} k G
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj (forget (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V))
      X)
    (CategoryTheory.Functor.map
      (forget (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)) f)
i : Functor.obj (forget (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V))
    X ≅
  Functor.obj (forget (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)) f)
e : X.ρ.Equiv Y.ρ :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toIntertwiningMap := __src, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯ }
⊢ IsIso f

Tactic:
(mkIso e).isIso_hom

Premises used: Rep.mkIso, CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X_1 Y_1 : Type w
inst_2 : AddCommGroup X_1
inst_3 : AddCommGroup Y_1
inst_4 : Module k X_1
inst_5 : Module k Y_1
ρ : Representation k G X_1
σ : Representation k G Y_1
A B C : Rep.{w, u, v} k G
Z : Type w
inst_6 : AddCommGroup Z
inst_7 : Module k Z
τ : Representation k G Z
X Y : Rep.{w, u, v} k G
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj (forget (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V))
      X)
    (CategoryTheory.Functor.map
      (forget (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)) f)
i : Functor.obj (forget (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V))
    X ≅
  Functor.obj (forget (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)) f)
e : X.ρ.Equiv Y.ρ :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toIntertwiningMap := __src, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯ }
⊢ IsIso f

Tactic:
exact (mkIso e).isIso_hom

Premises used: Rep.mkIso, CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
⊢ Function.Injective.{w + 1, w + 1} (α := A.Hom B) Hom.hom

Tactic:
hom_bijective.injective

Premises used: Rep.hom_bijective, Function.Bijective.injective
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
⊢ Function.Surjective.{w + 1, w + 1} (α := A.Hom B) Hom.hom

Tactic:
hom_bijective.surjective

Premises used: Rep.hom_bijective, Function.Bijective.surjective
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
f g : ρ.IntertwiningMap σ
⊢ ofHom (f + g) = ofHom f + ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
f g : A ⟶ B
⊢ Hom.hom (f + g) = Hom.hom f + Hom.hom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
f : A ⟶ B
g : B ⟶ C
⊢ (Hom.hom (f ≫ g)).toLinearMap = (Hom.hom g).toLinearMap ∘ₗ (Hom.hom f).toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
f₁ f₂ : A ⟶ B
g : B ⟶ C
hf : Hom.hom ((f₁ + f₂) ≫ g) = Hom.hom (f₁ ≫ g + f₂ ≫ g)
⊢ (f₁ + f₂) ≫ g = f₁ ≫ g + f₂ ≫ g

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
f₁ f₂ : A ⟶ B
g : B ⟶ C
⊢ Hom.hom ((f₁ + f₂) ≫ g) = Hom.hom (f₁ ≫ g + f₂ ≫ g)

Tactic:
simp [add_hom, Representation.IntertwiningMap.add_comp]

Premises used: Rep.add_hom, Representation.IntertwiningMap.add_comp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
f : A ⟶ B
g₁ g₂ : B ⟶ C
hf : Hom.hom (f ≫ (g₁ + g₂)) = Hom.hom (f ≫ g₁ + f ≫ g₂)
⊢ f ≫ (g₁ + g₂) = f ≫ g₁ + f ≫ g₂

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
f : A ⟶ B
g₁ g₂ : B ⟶ C
⊢ Hom.hom (f ≫ (g₁ + g₂)) = Hom.hom (f ≫ g₁ + f ≫ g₂)

Tactic:
simp [add_hom, Representation.IntertwiningMap.comp_add]

Premises used: Representation.IntertwiningMap.comp_add, Rep.add_hom
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
⊢ Eq.{w + 1} (α := of ρ ⟶ of σ) (ofHom 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
⊢ Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
f : ρ.IntertwiningMap σ
n : ℕ
⊢ ofHom (n • f) = n • ofHom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
f : A ⟶ B
n : ℕ
⊢ Hom.hom (n • f) = n • Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
f : ρ.IntertwiningMap σ
⊢ ofHom (-f) = -ofHom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
f : A ⟶ B
⊢ Hom.hom (-f) = -Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
f g : ρ.IntertwiningMap σ
⊢ ofHom (f - g) = ofHom f - ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
f g : A ⟶ B
⊢ Hom.hom (f - g) = Hom.hom f - Hom.hom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
f : ρ.IntertwiningMap σ
n : ℤ
⊢ ofHom (n • f) = n • ofHom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
f : A ⟶ B
n : ℤ
⊢ Hom.hom (n • f) = n • Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
ι : Type u'
f : ι → (A ⟶ B)
⊢ Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, Hom.hom (f i))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
ι : Type u'
f : ι → (A ⟶ B)
a : ι
s : Finset ι
ha : a ∉ s
h : Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ s, f i)) (∑ i ∈ s, Hom.hom (f i))
⊢ Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ insert a s, f i)) (∑ i ∈ insert a s, Hom.hom (f i))

Tactic:
simp [Finset.sum_insert ha, add_hom, h]

Premises used: Rep.add_hom, Finset.sum_insert
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
ι : Type u'
f : ι → (A ⟶ B)
s : Finset ι
empty : Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, Hom.hom (f i))
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (h : Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ s, f i)) (∑ i ∈ s, Hom.hom (f i))),
    Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ Insert.insert a s, f i))
      (∑ i ∈ Insert.insert a s, Hom.hom (f i))
⊢ Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ s, f i)) (∑ i ∈ s, Hom.hom (f i))

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert a s ha h => simp [Finset.sum_insert ha, add_hom, h]

Premises used: Rep.add_hom, Insert.insert
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
ι : Type u'
f : ι → (A ⟶ B)
s : Finset ι
empty : Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, Hom.hom (f i))
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (h : Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ s, f i)) (∑ i ∈ s, Hom.hom (f i))),
    Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ Insert.insert a s, f i))
      (∑ i ∈ Insert.insert a s, Hom.hom (f i))
⊢ Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ s, f i)) (∑ i ∈ s, Hom.hom (f i))

Tactic:
classical induction s using Finset.induction with
  | empty => simp
  | insert a s ha h => simp [Finset.sum_insert ha, add_hom, h]

Premises used: Rep.add_hom, Insert.insert
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
ι : Type u'
M N : Type v'
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module k M
inst_5 : Module k N
σ : Representation k G M
ρ : Representation k G N
f : ι → σ.IntertwiningMap ρ
⊢ Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, ofHom (f i))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
ι : Type u'
M N : Type v'
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module k M
inst_5 : Module k N
σ : Representation k G M
ρ : Representation k G N
f : ι → σ.IntertwiningMap ρ
a : ι
s : Finset ι
ha : a ∉ s
h : Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ s, f i)) (∑ i ∈ s, ofHom (f i))
⊢ Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ insert a s, f i)) (∑ i ∈ insert a s, ofHom (f i))

Tactic:
simp [Finset.sum_insert ha, ofHom_add, h]

Premises used: Rep.ofHom_add, Finset.sum_insert
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
ι : Type u'
M N : Type v'
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module k M
inst_5 : Module k N
σ : Representation k G M
ρ : Representation k G N
f : ι → σ.IntertwiningMap ρ
s : Finset ι
empty : Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, ofHom (f i))
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (h : Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ s, f i)) (∑ i ∈ s, ofHom (f i))),
    Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ Insert.insert a s, f i)) (∑ i ∈ Insert.insert a s, ofHom (f i))
⊢ Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ s, f i)) (∑ i ∈ s, ofHom (f i))

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert a s ha h => simp [Finset.sum_insert ha, ofHom_add, h]

Premises used: Rep.ofHom_add, Insert.insert
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
ι : Type u'
M N : Type v'
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module k M
inst_5 : Module k N
σ : Representation k G M
ρ : Representation k G N
f : ι → σ.IntertwiningMap ρ
s : Finset ι
empty : Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, ofHom (f i))
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (h : Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ s, f i)) (∑ i ∈ s, ofHom (f i))),
    Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ Insert.insert a s, f i)) (∑ i ∈ Insert.insert a s, ofHom (f i))
⊢ Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ s, f i)) (∑ i ∈ s, ofHom (f i))

Tactic:
classical induction s using Finset.induction with
  | empty => simp
  | insert a s ha h => simp [Finset.sum_insert ha, ofHom_add, h]

Premises used: Rep.ofHom_add, Insert.insert
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
V : Type w
inst_2 : AddCommGroup V
inst_3 : Module k V
⊢ (↑(trivial k G V) : Type w) = V

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
V : Type w
inst_2 : AddCommGroup V
inst_3 : Module k V
g : G
⊢ Eq.{w + 1} (α := (↑(trivial k G V) : Type w) →ₗ[k] (↑(trivial k G V) : Type w))
    (((ρ (trivial k G V) : Representation.{u, v, w} k G (↑(trivial k G V) : Type w)) :
          (a : G) → (↑(trivial k G V) : Type w) →ₗ[k] (↑(trivial k G V) : Type w))
        g :
      (↑(trivial k G V) : Type w) →ₗ[k] (↑(trivial k G V) : Type w))
    (LinearMap.id : (↑(trivial k G V) : Type w) →ₗ[k] (↑(trivial k G V) : Type w))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
V : Type w
inst_2 : AddCommGroup V
inst_3 : Module k V
g : G
v : V
⊢ ((((ρ (trivial k G V) : Representation.{u, v, w} k G (↑(trivial k G V) : Type w)) :
              (a : G) → (↑(trivial k G V) : Type w) →ₗ[k] (↑(trivial k G V) : Type w))
            g :
          (↑(trivial k G V) : Type w) →ₗ[k] (↑(trivial k G V) : Type w)) :
        (a : (↑(trivial k G V) : Type w)) → (↑(trivial k G V) : Type w))
      v =
    v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A : Rep.{w, u, v} k G
g1 g2 : G
h :
  ∀ (x : (↑A : Type w)),
    Eq (α := (↑A : Type w))
      ((((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) (g1 * g2) : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
            (a : (↑A : Type w)) → (↑A : Type w))
          x :
        (↑A : Type w))
      (((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g1 ∘ₗ
              (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g2 :
            (a : (↑A : Type w)) → (↑A : Type w))
          x :
        (↑A : Type w))
⊢ Eq.{w + 1} (α := (↑A : Type w) →ₗ[k] (↑A : Type w))
    ((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) (g1 * g2) : (↑A : Type w) →ₗ[k] (↑A : Type w))
    ((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g1 ∘ₗ (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g2 :
      (↑A : Type w) →ₗ[k] (↑A : Type w))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A : Rep.{w, u, v} k G
g1 g2 : G
x : (↑A : Type w)
⊢ Eq (α := (↑A : Type w))
    ((((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) (g1 * g2) : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        x :
      (↑A : Type w))
    (((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g1 ∘ₗ (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g2 :
          (a : (↑A : Type w)) → (↑A : Type w))
        x :
      (↑A : Type w))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G_1 : Type v
inst : Semiring k
inst_1 : Monoid G_1
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G_1 X
σ : Representation k G_1 Y
A_1 B C : Rep.{w, u, v} k G_1
Z : Type w
inst_6 : AddCommGroup Z
inst_7 : Module k Z
τ : Representation k G_1 Z
G : Type v
inst_8 : CommMonoid G
A : Rep.{u_1, u, v} k G
g : G
⊢ ∀ (g_1 : G),
    Eq.{u_1 + 1} (α := (↑A : Type u_1) →ₗ[k] (↑A : Type u_1))
      ((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g ∘ₗ
        (A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g_1)
      ((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g_1 ∘ₗ
        (A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g)

Tactic:
simp [← ρ_mul, mul_comm]

Premises used: Rep.ρ_mul, mul_comm
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : Semiring k
G : Type v
inst_1 : CommMonoid G
A : Rep.{u_1, u, v} k G
g : G
x : (↑A : Type u_1)
⊢ Eq (α := (↑A : Type u_1)) ((Hom.hom (A.applyAsHom g) : (a : (↑A : Type u_1)) → (↑A : Type u_1)) x : (↑A : Type u_1))
    ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
          (a : (↑A : Type u_1)) → (↑A : Type u_1))
        x :
      (↑A : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : Semiring k
G : Type v
inst_1 : CommMonoid G
A B : Rep.{u_1, u, v} k G
f : A ⟶ B
g : G
hf :
  ∀ (x : (↑A : Type u_1)),
    Eq (α := (↑B : Type u_1))
      (((Hom.hom (A.applyAsHom g ≫ f)).toLinearMap : (a : (↑A : Type u_1)) → (↑B : Type u_1)) x : (↑B : Type u_1))
      (((Hom.hom (f ≫ B.applyAsHom g)).toLinearMap : (a : (↑A : Type u_1)) → (↑B : Type u_1)) x : (↑B : Type u_1))
⊢ A.applyAsHom g ≫ f = f ≫ B.applyAsHom g

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : Semiring k
G : Type v
inst_1 : CommMonoid G
A B : Rep.{u_1, u, v} k G
f : A ⟶ B
g : G
x : (↑A : Type u_1)
⊢ Eq (α := (↑B : Type u_1))
    (((Hom.hom (A.applyAsHom g ≫ f)).toLinearMap : (a : (↑A : Type u_1)) → (↑B : Type u_1)) x : (↑B : Type u_1))
    (((Hom.hom (f ≫ B.applyAsHom g)).toLinearMap : (a : (↑A : Type u_1)) → (↑B : Type u_1)) x : (↑B : Type u_1))

Tactic:
simp [hom_comm_apply]

Premises used: Rep.hom_comm_apply
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A : Type w'
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
g : G
a : A
⊢ ((((ρ (ofDistribMulAction k G A) : Representation.{u, v, w'} k G (↑(ofDistribMulAction k G A) : Type w')) :
              (a : G) → (↑(ofDistribMulAction k G A) : Type w') →ₗ[k] (↑(ofDistribMulAction k G A) : Type w'))
            g :
          (↑(ofDistribMulAction k G A) : Type w') →ₗ[k] (↑(ofDistribMulAction k G A) : Type w')) :
        (a : (↑(ofDistribMulAction k G A) : Type w')) → (↑(ofDistribMulAction k G A) : Type w'))
      a =
    g • a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
M : Type u_1
G : Type u_2
inst : Monoid M
inst_1 : CommGroup G
inst_2 : MulDistribMulAction M G
g : M
a : Additive G
⊢ Eq (α := (↑(ofMulDistribMulAction M G) : Type u_2))
    (((((ρ (ofMulDistribMulAction M G) : Representation.{0, u_1, u_2} ℤ M (↑(ofMulDistribMulAction M G) : Type u_2)) :
                (a : M) → (↑(ofMulDistribMulAction M G) : Type u_2) →ₗ[ℤ] (↑(ofMulDistribMulAction M G) : Type u_2))
              g :
            (↑(ofMulDistribMulAction M G) : Type u_2) →ₗ[ℤ] (↑(ofMulDistribMulAction M G) : Type u_2)) :
          (a : (↑(ofMulDistribMulAction M G) : Type u_2)) → (↑(ofMulDistribMulAction M G) : Type u_2))
        a :
      (↑(ofMulDistribMulAction M G) : Type u_2))
    ((Additive.ofMul : (a : G) → Additive G) (HSMul.hSMul (β := G) g ((Additive.toMul : (a : Additive G) → G) a : G)) :
      Additive G)

Tactic:
rfl

Premises used: rfl