awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
M : Type u_4
inst_2 : AddCommMonoid M
inst_3 : Module k[G] M
r : k[G]
m : asModule.{u_1, u_2, u_4} (k := k) (G := G) (V := RestrictScalars k k[G] M) (ofModule M)
dsimp :
  (RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M)
      ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) r :
              End k (RestrictScalars k k[G] M)) :
            (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
          ((asModuleEquiv (ofModule M) : (a : (ofModule M).asModule) → RestrictScalars k k[G] M) m :
            RestrictScalars k k[G] M) :
        RestrictScalars k k[G] M) =
    HSMul.hSMul (β := M) r
      ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M)
          ((asModuleEquiv (ofModule M) : (a : (ofModule M).asModule) → RestrictScalars k k[G] M) m :
            RestrictScalars k k[G] M) :
        M)
⊢ (RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M)
      ((asModuleEquiv (ofModule M) : (a : (ofModule M).asModule) → RestrictScalars k k[G] M) (r • m) :
        RestrictScalars k k[G] M) =
    HSMul.hSMul (β := M) r
      ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M)
          ((asModuleEquiv (ofModule M) : (a : (ofModule M).asModule) → RestrictScalars k k[G] M) m :
            RestrictScalars k k[G] M) :
        M)

Tactic:
dsimp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
M : Type u_4
inst_2 : AddCommMonoid M
inst_3 : Module k[G] M
r : k[G]
m : asModule.{u_1, u_2, u_4} (k := k) (G := G) (V := RestrictScalars k k[G] M) (ofModule M)
⊢ (RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M)
      ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) r :
              End k (RestrictScalars k k[G] M)) :
            (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
          ((asModuleEquiv (ofModule M) : (a : (ofModule M).asModule) → RestrictScalars k k[G] M) m :
            RestrictScalars k k[G] M) :
        RestrictScalars k k[G] M) =
    HSMul.hSMul (β := M) r
      ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M)
          ((asModuleEquiv (ofModule M) : (a : (ofModule M).asModule) → RestrictScalars k k[G] M) m :
            RestrictScalars k k[G] M) :
        M)

Tactic:
simp only [AddEquiv.apply_symm_apply, ofModule_asAlgebraHom_apply_apply]

Premises used: AddEquiv.apply_symm_apply, Representation.ofModule_asAlgebraHom_apply_apply
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
t : k
g : G
v : ρ.asModule
rw :
  HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g t) v =
    (ρ.asModuleEquiv : (a : ρ.asModule) → V) (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g t) v)
⊢ HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g t) v =
    HSMul.hSMul (β := V) t
      ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) ((ρ.asModuleEquiv : (a : ρ.asModule) → V) v : V) : V)

Tactic:
rw [← LinearMap.smul_apply, ← asAlgebraHom_single, ← asModuleEquiv_map_smul]

Premises used: Representation.asAlgebraHom_single, LinearMap.smul_apply, Representation.asModuleEquiv_map_smul
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
t : k
g : G
v : ρ.asModule
⊢ HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g t) v =
    (ρ.asModuleEquiv : (a : ρ.asModule) → V) (HSMul.hSMul (α := k[G]) (MonoidAlgebra.single g t) v)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
t : k
x : k[G]
v : ρ.asModule
revert : ∀ (t : k), (t • x) • v = t • x • v
⊢ (t • x) • v = t • x • v

Tactic:
revert t
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
hM :
  ∀ (m : G) (t : k),
    HSMul.hSMul (β := k[G]) t ((of k G : (a : G) → k[G]) m : k[G]) • v =
      t • HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) m : k[G]) v
hadd :
  ∀ (x y : k[G]),
    (∀ (t : k), (t • x) • v = t • x • v) →
      (∀ (t : k), (t • y) • v = t • y • v) → ∀ (t : k), (t • (x + y)) • v = t • (x + y) • v
hsmul : ∀ (r : k) (x : k[G]), (∀ (t : k), (t • x) • v = t • x • v) → ∀ (t : k), (t • r • x) • v = t • (r • x) • v
⊢ ∀ (t : k), (t • x) • v = t • x • v

Tactic:
apply x.induction_on

Premises used: MonoidAlgebra.induction_on
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
⊢ ∀ (m : G) (t : k),
    HSMul.hSMul (β := k[G]) t ((of k G : (a : G) → k[G]) m : k[G]) • v =
      t • HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) m : k[G]) v

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
y z : k[G]
hy : ∀ (t : k), (t • y) • v = t • y • v
hz : ∀ (t : k), (t • z) • v = t • z • v
⊢ ∀ (t : k), (t • (y + z)) • v = t • (y + z) • v

Tactic:
simp [add_smul, hy, hz]

Premises used: add_smul
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
s : k
y : k[G]
hy : ∀ (t : k), (t • y) • v = t • y • v
t : k
hsmul : t • s • y • v = t • (s • y) • v
⊢ (t • s • y) • v = t • (s • y) • v

Tactic:
rw [← smul_assoc, smul_eq_mul, hy (t * s), ← smul_eq_mul, smul_assoc]

Premises used: HMul.hMul, smul_assoc, smul_eq_mul
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
s : k
y : k[G]
hy : ∀ (t : k), (t • y) • v = t • y • v
t : k
⊢ t • s • y • v = t • (s • y) • v

Tactic:
aesop
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : AddCommMonoid V
inst_4 : Module k V
ρ : Representation k G V
g : G
h : ∀ (x : V), Eq (α := V) ((ρ.norm ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g : (a : V) → V) x : V) ((ρ.norm : (a : V) → V) x : V)
⊢ ρ.norm ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g = ρ.norm

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : AddCommMonoid V
inst_4 : Module k V
ρ : Representation k G V
g : G
x : V
⊢ ∀ (x_1 : G),
    Eq (α := V)
      ((((ρ : (a : G) → V →ₗ[k] V) x_1 : V →ₗ[k] V) : (a : V) → V)
          ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V) :
        V)
      (((ρ : (a : G) → V →ₗ[k] V) ((fun (x : G) ↦ x * g) x_1) : (a : V) → V) x : V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : AddCommMonoid V
inst_4 : Module k V
ρ : Representation k G V
g : G
x : V
⊢ Eq (α := V) ((ρ.norm ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g : (a : V) → V) x : V) ((ρ.norm : (a : V) → V) x : V)

Tactic:
simpa [norm] using Fintype.sum_bijective (· * g) (Group.mulRight_bijective g) _ _ <| by simp

Premises used: HMul.hMul, Fintype.sum_bijective, Group.mulRight_bijective, Representation.norm
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : AddCommMonoid V
inst_4 : Module k V
ρ : Representation k G V
g : G
x : V
⊢ Eq (α := V) ((ρ.norm : (a : V) → V) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V) : V)
    ((ρ.norm : (a : V) → V) x : V)

Tactic:
LinearMap.ext_iff.1 (norm_comp_self _ _) x

Premises used: LinearMap.ext_iff, Representation.norm_comp_self, Iff.mp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : AddCommMonoid V
inst_4 : Module k V
ρ : Representation k G V
g : G
h : ∀ (x : V), Eq (α := V) (((ρ : (a : G) → V →ₗ[k] V) g ∘ₗ ρ.norm : (a : V) → V) x : V) ((ρ.norm : (a : V) → V) x : V)
⊢ (ρ : (a : G) → V →ₗ[k] V) g ∘ₗ ρ.norm = ρ.norm

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : AddCommMonoid V
inst_4 : Module k V
ρ : Representation k G V
g : G
x : V
⊢ ∀ (x_1 : G),
    Eq (α := V)
      ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V)
          ((((ρ : (a : G) → V →ₗ[k] V) x_1 : V →ₗ[k] V) : (a : V) → V) x : V) :
        V)
      (((ρ : (a : G) → V →ₗ[k] V) ((fun (x : G) ↦ g * x) x_1) : (a : V) → V) x : V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : AddCommMonoid V
inst_4 : Module k V
ρ : Representation k G V
g : G
x : V
⊢ Eq (α := V) (((ρ : (a : G) → V →ₗ[k] V) g ∘ₗ ρ.norm : (a : V) → V) x : V) ((ρ.norm : (a : V) → V) x : V)

Tactic:
simpa [norm] using Fintype.sum_bijective (g * ·) (Group.mulLeft_bijective g) _ _ <| by simp

Premises used: HMul.hMul, Group.mulLeft_bijective, Fintype.sum_bijective, Representation.norm
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : AddCommMonoid V
inst_4 : Module k V
ρ : Representation k G V
g : G
x : V
⊢ Eq (α := V) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) ((ρ.norm : (a : V) → V) x : V) : V)
    ((ρ.norm : (a : V) → V) x : V)

Tactic:
LinearMap.ext_iff.1 (self_comp_norm _ _) x

Premises used: LinearMap.ext_iff, Iff.mp, Representation.self_comp_norm
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (σ₁₂ := RingHom.id k) ((ρ : (a : G) → V →ₗ[k] V) g) W
h :
  ∀ (x : ↥W),
    Eq.{u_3 + 1} (α := V) (↑((restrict ((ρ : (a : G) → V →ₗ[k] V) 1) ⋯ : (a : ↥W) → ↥W) x) : V)
      (↑((1 : (a : ↥W) → ↥W) x) : V)
⊢ restrict ((ρ : (a : G) → V →ₗ[k] V) 1) ⋯ = 1

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (σ₁₂ := RingHom.id k) ((ρ : (a : G) → V →ₗ[k] V) g) W
x : ↥W
⊢ Eq.{u_3 + 1} (α := V) (↑((restrict ((ρ : (a : G) → V →ₗ[k] V) 1) ⋯ : (a : ↥W) → ↥W) x) : V)
    (↑((1 : (a : ↥W) → ↥W) x) : V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (σ₁₂ := RingHom.id k) ((ρ : (a : G) → V →ₗ[k] V) g) W
x x_1 : G
h :
  ∀ (x_2 : ↥W),
    Eq.{u_3 + 1} (α := V) (↑((restrict ((ρ : (a : G) → V →ₗ[k] V) (x * x_1)) ⋯ : (a : ↥W) → ↥W) x_2) : V)
      (↑((restrict ((ρ : (a : G) → V →ₗ[k] V) x) ⋯ * restrict ((ρ : (a : G) → V →ₗ[k] V) x_1) ⋯ : (a : ↥W) → ↥W) x_2) :
        V)
⊢ restrict ((ρ : (a : G) → V →ₗ[k] V) (x * x_1)) ⋯ =
    restrict ((ρ : (a : G) → V →ₗ[k] V) x) ⋯ * restrict ((ρ : (a : G) → V →ₗ[k] V) x_1) ⋯

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (σ₁₂ := RingHom.id k) ((ρ : (a : G) → V →ₗ[k] V) g) W
x x_1 : G
x_2 : ↥W
⊢ Eq.{u_3 + 1} (α := V) (↑((restrict ((ρ : (a : G) → V →ₗ[k] V) (x * x_1)) ⋯ : (a : ↥W) → ↥W) x_2) : V)
    (↑((restrict ((ρ : (a : G) → V →ₗ[k] V) x) ⋯ * restrict ((ρ : (a : G) → V →ₗ[k] V) x_1) ⋯ : (a : ↥W) → ↥W) x_2) : V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Ring k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (σ₁₂ := RingHom.id k) ((ρ : (a : G) → V →ₗ[k] V) g) W
h :
  ∀ (x : V),
    Eq (α := V ⧸ W) ((W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) 1) ⋯ ∘ₗ W.mkQ : (a : V) → V ⧸ W) x : V ⧸ W)
      ((1 ∘ₗ W.mkQ : (a : V) → V ⧸ W) x : V ⧸ W)
⊢ W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) 1) ⋯ = 1

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Ring k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (σ₁₂ := RingHom.id k) ((ρ : (a : G) → V →ₗ[k] V) g) W
x : V
⊢ Eq (α := V ⧸ W) ((W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) 1) ⋯ ∘ₗ W.mkQ : (a : V) → V ⧸ W) x : V ⧸ W)
    ((1 ∘ₗ W.mkQ : (a : V) → V ⧸ W) x : V ⧸ W)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Ring k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (σ₁₂ := RingHom.id k) ((ρ : (a : G) → V →ₗ[k] V) g) W
x x_1 : G
h :
  ∀ (x_2 : V),
    Eq (α := V ⧸ W) ((W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) (x * x_1)) ⋯ ∘ₗ W.mkQ : (a : V) → V ⧸ W) x_2 : V ⧸ W)
      (((W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) x) ⋯ * W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) x_1) ⋯) ∘ₗ W.mkQ :
            (a : V) → V ⧸ W)
          x_2 :
        V ⧸ W)
⊢ W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) (x * x_1)) ⋯ =
    W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) x) ⋯ * W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) x_1) ⋯

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Ring k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
W : Submodule k V
le_comap : ∀ (g : G), W ≤ Submodule.comap (σ₁₂ := RingHom.id k) ((ρ : (a : G) → V →ₗ[k] V) g) W
x x_1 : G
x_2 : V
⊢ Eq (α := V ⧸ W) ((W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) (x * x_1)) ⋯ ∘ₗ W.mkQ : (a : V) → V ⧸ W) x_2 : V ⧸ W)
    (((W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) x) ⋯ * W.mapQ W ((ρ : (a : G) → V →ₗ[k] V) x_1) ⋯) ∘ₗ W.mkQ :
          (a : V) → V ⧸ W)
        x_2 :
      V ⧸ W)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_4 : IsTrivial (MonoidHom.comp ρ S.subtype)
g h : G
hgh : Eq (α := G ⧸ S) (↑g : G ⧸ S) (↑h : G ⧸ S)
h₁ :
  ∀ (x : V),
    Eq (α := V) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V)
      ((((ρ : (a : G) → V →ₗ[k] V) h : V →ₗ[k] V) : (a : V) → V) x : V)
⊢ Eq.{u_3 + 1} (α := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) h : V →ₗ[k] V)

Tactic:
ext x
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_4 : IsTrivial (MonoidHom.comp ρ S.subtype)
g h : G
hgh : Eq (α := G ⧸ S) (↑g : G ⧸ S) (↑h : G ⧸ S)
x : V
h₁ :
  Eq (α := V)
    ((((ρ : (a : G) → V →ₗ[k] V) g⁻¹ : V →ₗ[k] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V) :
      V)
    ((((ρ : (a : G) → V →ₗ[k] V) g⁻¹ : V →ₗ[k] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[k] V) h : V →ₗ[k] V) : (a : V) → V) x : V) :
      V)
⊢ Eq (α := V) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V)
    ((((ρ : (a : G) → V →ₗ[k] V) h : V →ₗ[k] V) : (a : V) → V) x : V)

Tactic:
apply (ρ.apply_bijective g⁻¹).1

Premises used: Representation.apply_bijective, Inv.inv, And.left
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_4 : IsTrivial (MonoidHom.comp ρ S.subtype)
g h : G
hgh : Eq (α := G ⧸ S) (↑g : G ⧸ S) (↑h : G ⧸ S)
x : V
⊢ Eq (α := V)
    ((((ρ : (a : G) → V →ₗ[k] V) g⁻¹ : V →ₗ[k] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V) :
      V)
    ((((ρ : (a : G) → V →ₗ[k] V) g⁻¹ : V →ₗ[k] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[k] V) h : V →ₗ[k] V) : (a : V) → V) x : V) :
      V)

Tactic:
simpa [← Module.End.mul_apply, ← map_mul, -isTrivial_def] using
    (congr($(isTrivial_def (ρ.comp S.subtype) ⟨g⁻¹ * h, QuotientGroup.eq.1 hgh⟩) x)).symm

Premises used: HMul.hMul, congrArg, Subgroup.subtype, QuotientGroup.eq, id, MonoidHom.comp, Subtype.mk, map_mul, Representation.isTrivial_def, Inv.inv, Iff.mp, Module.End.mul_apply, Eq.symm, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_4 : S.Normal
inst_5 : IsTrivial (MonoidHom.comp ρ S.subtype)
y : G
z : Gᵐᵒᵖ
hz : z ∈ S.op
h :
  ∀ (w : V),
    Eq (α := V)
      (((ρ : (a : G) → V →ₗ[k] V) ((fun (m : ↥S.op) ↦ m • y) (Subtype.mk (p := fun (x : Gᵐᵒᵖ) ↦ x ∈ S.op) z hz)) :
            (a : V) → V)
          w :
        V)
      ((((ρ : (a : G) → V →ₗ[k] V) y : V →ₗ[k] V) : (a : V) → V) w : V)
⊢ (Con.ker ρ : (a : G) → G → Prop) ((fun (m : ↥S.op) ↦ m • y) (Subtype.mk (p := fun (x : Gᵐᵒᵖ) ↦ x ∈ S.op) z hz)) y

Tactic:
ext w
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_4 : S.Normal
inst_5 : IsTrivial (MonoidHom.comp ρ S.subtype)
y : G
z : Gᵐᵒᵖ
hz : z ∈ S.op
w : V
h :
  Eq (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (y * MulOpposite.unop z) : V →ₗ[k] V) : (a : V) → V) w : V)
    ((((ρ : (a : G) → V →ₗ[k] V) y : V →ₗ[k] V) : (a : V) → V) w : V)
⊢ Eq (α := V)
    (((ρ : (a : G) → V →ₗ[k] V) ((fun (m : ↥S.op) ↦ m • y) (Subtype.mk (p := fun (x : Gᵐᵒᵖ) ↦ x ∈ S.op) z hz)) :
          (a : V) → V)
        w :
      V)
    ((((ρ : (a : G) → V →ₗ[k] V) y : V →ₗ[k] V) : (a : V) → V) w : V)

Tactic:
change ρ (_ * z.unop) _ = _

Premises used: HMul.hMul, MulOpposite.unop, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_4 : S.Normal
inst_5 : IsTrivial (MonoidHom.comp ρ S.subtype)
y : G
z : Gᵐᵒᵖ
hz : z ∈ S.op
w : V
⊢ Eq (α := G ⧸ S) (↑(y * MulOpposite.unop z) : G ⧸ S) (↑y : G ⧸ S)

Tactic:
simp_all
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_4 : S.Normal
inst_5 : IsTrivial (MonoidHom.comp ρ S.subtype)
y : G
z : Gᵐᵒᵖ
hz : z ∈ S.op
w : V
⊢ Eq (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (y * MulOpposite.unop z) : V →ₗ[k] V) : (a : V) → V) w : V)
    ((((ρ : (a : G) → V →ₗ[k] V) y : V →ₗ[k] V) : (a : V) → V) w : V)

Tactic:
exact congr($(apply_eq_of_coe_eq ρ S _ _ (by simp_all)) w)
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring k
inst_1 : Group G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_4 : S.Normal
inst_5 : IsTrivial (MonoidHom.comp ρ S.subtype)
g : G
x : V
⊢ Eq (α := V)
    (((((ρ.ofQuotient S : Representation.{u_1, u_2, u_3} k (G ⧸ S) V) : (a : G ⧸ S) → V →ₗ[k] V) (↑g : G ⧸ S) :
            V →ₗ[k] V) :
          (a : V) → V)
        x :
      V)
    ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Ring k
inst_1 : Monoid G
I : AddCommGroup V
inst_2 : Module k V
ρ : Representation k G V
g : G
x : V
⊢ (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
      (Fin.partialSum (n := HAdd.hAdd (α := ℕ) 0 1)
        (fun (j : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦
          (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x)
        (Fin.last (HAdd.hAdd (α := ℕ) 0 1))) =
    HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (g ^ HAdd.hAdd (α := ℕ) 0 1) : V →ₗ[k] V) : (a : V) → V) x : V) x

Tactic:
simp [Fin.partialSum]

Premises used: Fin.partialSum
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Ring k
inst_1 : Monoid G
I : AddCommGroup V
inst_2 : Module k V
ρ : Representation k G V
g : G
x : V
n : ℕ
h :
  (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
      (Fin.partialSum (n := n + 1)
        (fun (j : Fin (n + 1)) ↦ (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x)
        (Fin.last (n + 1))) =
    HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (n + 1)) : V →ₗ[k] V) : (a : V) → V) x : V) x
h₁ :
  ∀ (x_1 : Fin (n + 1)),
    Eq.{u_3 + 1} (α := V)
      (Fin.init (α := fun (j : Fin (n + 2)) ↦ V)
          (fun (j : Fin (n + 2)) ↦ (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x) x_1 :
        V)
      ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑x_1 : ℕ)) : V →ₗ[k] V) : (a : V) → V) x : V)
⊢ Eq.{u_3 + 1} (α := (i : Fin (n + 1)) → V)
    (Fin.init (α := fun (j : Fin (n + 2)) ↦ V) fun (j : Fin (n + 2)) ↦
        (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x :
      (i : Fin (n + 1)) → V)
    fun (j : Fin (n + 1)) ↦ ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x : V)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Basic
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Ring k
inst_1 : Monoid G
I : AddCommGroup V
inst_2 : Module k V
ρ : Representation k G V
g : G
x : V
n : ℕ
h :
  (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
      (Fin.partialSum (n := n + 1)
        (fun (j : Fin (n + 1)) ↦ (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x)
        (Fin.last (n + 1))) =
    HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (n + 1)) : V →ₗ[k] V) : (a : V) → V) x : V) x
x_1 : Fin (n + 1)
⊢ Eq.{u_3 + 1} (α := V)
    (Fin.init (α := fun (j : Fin (n + 2)) ↦ V)
        (fun (j : Fin (n + 2)) ↦ (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) x) x_1 :
      V)
    ((((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑x_1 : ℕ)) : V →ₗ[k] V) : (a : V) → V) x : V)

Tactic:
simp [Fin.init]

Premises used: Fin.init