awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ψ : ρ.Equiv σ
toIntertwiningMap : ρ.IntertwiningMap σ
invFun : W → V
left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun
right_inv : Function.RightInverse invFun toIntertwiningMap.toFun
h :
  Eq (α := (a : V) → W)
    (⇑{ toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
          ρ.Equiv σ } :
      (a : V) → W)
    (⇑ψ : (a : V) → W)
mk' :
  ∀ (toIntertwiningMap_1 : ρ.IntertwiningMap σ) (invFun_1 : W → V)
    (left_inv_1 : Function.LeftInverse invFun_1 toIntertwiningMap_1.toFun)
    (right_inv_1 : Function.RightInverse invFun_1 toIntertwiningMap_1.toFun)
    (h :
      Eq (α := (a : V) → W)
        (⇑{ toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
              ρ.Equiv σ } :
          (a : V) → W)
        (⇑{ toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1,
              right_inv := right_inv_1 : ρ.Equiv σ } :
          (a : V) → W)),
    { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
        ρ.Equiv σ } =
      { toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }
⊢ { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
      ρ.Equiv σ } =
    ψ

Tactic:
cases ψ
-- 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
toIntertwiningMap : ρ.IntertwiningMap σ
invFun : W → V
left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun
right_inv : Function.RightInverse invFun toIntertwiningMap.toFun
toIntertwiningMap_1 : ρ.IntertwiningMap σ
invFun_1 : W → V
left_inv_1 : Function.LeftInverse invFun_1 toIntertwiningMap_1.toFun
right_inv_1 : Function.RightInverse invFun_1 toIntertwiningMap_1.toFun
h :
  Eq (α := (a : V) → W)
    (⇑{ toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
          ρ.Equiv σ } :
      (a : V) → W)
    (⇑{ toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 :
          ρ.Equiv σ } :
      (a : V) → W)
⊢ { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
      ρ.Equiv σ } =
    { toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_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
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
φ : ρ.Equiv σ
g : G
⊢ Eq (α := V →ₗ[A] V) ((↑(LinearEquiv.refl A V) : V →ₗ[A] V) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g)
    ((ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑(LinearEquiv.refl A V) : V →ₗ[A] V))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
⊢ (↑(refl ρ) : ρ.IntertwiningMap ρ) = IntertwiningMap.id ρ

Tactic:
rfl

Premises used: Representation.IntertwiningMap.id, rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
⊢ (↑(refl ρ) : ρ.IntertwiningMap ρ).toLinearMap = LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
v : V
⊢ (refl ρ : (a : V) → V) v = v

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
φ : ρ.Equiv σ
⊢ Eq (α := (a : V) → W) (⇑(↑φ : ρ.IntertwiningMap σ) : (a : V) → W) (⇑φ : (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
φ : ρ.Equiv σ
⊢ Eq (α := (a : V) → W) (⇑(↑φ : ρ.IntertwiningMap σ).toLinearMap : (a : V) → W) (⇑φ : (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
φ : ρ.Equiv σ
⊢ φ.invFun = (⇑φ.toLinearEquiv.symm : (a : W) → V)

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
φ : ρ.Equiv σ
⊢ (↑φ.toLinearEquiv : V →ₗ[A] W) = (↑φ : ρ.IntertwiningMap σ).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
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
φ : ρ.Equiv σ
v : V
⊢ Eq.{u_4 + 1} (α := W) ((φ.toLinearEquiv : (a : V) → W) v : W) (((↑φ : ρ.IntertwiningMap σ) : (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
φ_1 φ : ρ.Equiv σ
g : G
rw :
  (↑φ.toLinearEquiv : V →ₗ[A] W) ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g =
    (↑φ.toLinearEquiv : V →ₗ[A] W) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V)
rw₁ :
  ((↑φ.toLinearEquiv : V →ₗ[A] W) ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V)) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g =
    (↑φ.toLinearEquiv : V →ₗ[A] W) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V)
rw₂ :
  ((↑φ.toLinearEquiv : V →ₗ[A] W) ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V)) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g =
    ((↑φ.toLinearEquiv : V →ₗ[A] W) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g) ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V)
rw₃ :
  ((↑φ.toLinearEquiv : V →ₗ[A] W) ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V)) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g =
    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑φ : ρ.IntertwiningMap σ).toLinearMap) ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V)
rw₄ :
  Eq (α := W →ₗ[A] W) (LinearMap.id ∘ₗ (σ : (a : G) → W →ₗ[A] W) g)
    (((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑φ : ρ.IntertwiningMap σ).toLinearMap) ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V))
rw₅ :
  Eq (α := W →ₗ[A] W) (LinearMap.id ∘ₗ (σ : (a : G) → W →ₗ[A] W) g)
    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑φ : ρ.IntertwiningMap σ).toLinearMap ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V))
rw₆ :
  Eq.{u_4 + 1} (α := W →ₗ[A] W) (LinearMap.id ∘ₗ (σ : (a : G) → W →ₗ[A] W) g)
    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ LinearMap.id)
rw₇ :
  Eq.{u_4 + 1} (α := W →ₗ[A] W) ((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W)
    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ LinearMap.id : W →ₗ[A] W)
rw₈ rw₉ :
  Eq.{u_4 + 1} (α := W →ₗ[A] W) ((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) ((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W)
⊢ (↑φ.toLinearEquiv.symm : W →ₗ[A] V) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g =
    (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V)

Tactic:
rw [← cancel_left φ.toLinearEquiv.injective, ← comp_assoc, ← comp_assoc, φ.1.2 g, φ.comp_symm,
      comp_assoc, φ.comp_symm, id_comp, comp_id]

Premises used: LinearMap.comp_assoc, LinearEquiv.comp_symm, Representation.Equiv.toLinearEquiv, Representation.IntertwiningMap.isIntertwining', Representation.Equiv.toIntertwiningMap, LinearMap.comp_id, LinearEquiv.injective, LinearMap.id_comp, LinearMap.cancel_left
-- 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
e : V ≃ₗ[A] W
he : ∀ (g : G), (↑e : V →ₗ[A] W) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑e : V →ₗ[A] W)
g : G
apply :
  (↑e : V →ₗ[A] W) ∘ₗ (↑e.symm : W →ₗ[A] V) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g =
    (↑e : V →ₗ[A] W) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑e.symm : W →ₗ[A] V)
⊢ (↑e.symm : W →ₗ[A] V) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g = (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑e.symm : W →ₗ[A] V)

Tactic:
apply e.comp_toLinearMap_eq_iff _ _ |>.1

Premises used: LinearEquiv.comp_toLinearMap_eq_iff, Iff.mp
-- 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
e : V ≃ₗ[A] W
he : ∀ (g : G), (↑e : V →ₗ[A] W) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑e : V →ₗ[A] W)
g : G
rw :
  ((↑e : V →ₗ[A] W) ∘ₗ (↑e.symm : W →ₗ[A] V)) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g =
    (↑e : V →ₗ[A] W) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑e.symm : W →ₗ[A] V)
rw₁ :
  ((↑e : V →ₗ[A] W) ∘ₗ (↑e.symm : W →ₗ[A] V)) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g =
    ((↑e : V →ₗ[A] W) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g) ∘ₗ (↑e.symm : W →ₗ[A] V)
rw₂ :
  ((↑e : V →ₗ[A] W) ∘ₗ (↑e.symm : W →ₗ[A] V)) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g =
    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑e : V →ₗ[A] W)) ∘ₗ (↑e.symm : W →ₗ[A] V)
rw₃ :
  Eq (α := W →ₗ[A] W) (LinearMap.id ∘ₗ (σ : (a : G) → W →ₗ[A] W) g)
    (((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑e : V →ₗ[A] W)) ∘ₗ (↑e.symm : W →ₗ[A] V))
rw₄ :
  Eq.{u_4 + 1} (α := W →ₗ[A] W) ((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W)
    (((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑e : V →ₗ[A] W)) ∘ₗ (↑e.symm : W →ₗ[A] V) : W →ₗ[A] W)
rw₅ :
  Eq.{u_4 + 1} (α := W →ₗ[A] W) ((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W)
    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑e : V →ₗ[A] W) ∘ₗ (↑e.symm : W →ₗ[A] V) : W →ₗ[A] W)
rw₆ :
  Eq.{u_4 + 1} (α := W →ₗ[A] W) ((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W)
    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ LinearMap.id : W →ₗ[A] W)
rw₇ rw₈ :
  Eq.{u_4 + 1} (α := W →ₗ[A] W) ((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) ((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W)
⊢ (↑e : V →ₗ[A] W) ∘ₗ (↑e.symm : W →ₗ[A] V) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g =
    (↑e : V →ₗ[A] W) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑e.symm : W →ₗ[A] V)

Tactic:
rw [← comp_assoc, ← comp_assoc, he g, e.comp_symm, id_comp, comp_assoc, e.comp_symm, comp_id]

Premises used: LinearMap.comp_assoc, LinearEquiv.comp_symm, LinearMap.comp_id, LinearMap.id_comp
-- 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
e : V ≃ₗ[A] W
he : ∀ (g : G), (↑e : V →ₗ[A] W) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑e : V →ₗ[A] W)
⊢ (mk e he).symm = mk e.symm ⋯

Tactic:
rfl

Premises used: Representation.Equiv.symm, Representation.Equiv.mk, 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
φ : ρ.Equiv σ
⊢ (↑φ.symm : σ.IntertwiningMap ρ).toLinearMap = (↑φ.toLinearEquiv.symm : W →ₗ[A] V)

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
φ : ρ.Equiv σ
⊢ Eq (α := (a : W) → V) (⇑φ.toLinearEquiv.symm : (a : W) → V) (⇑φ.symm : (a : W) → V)

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
φ_1 φ : ρ.Equiv σ
ψ : σ.Equiv τ
g : G
rw :
  ((↑ψ.toLinearEquiv : W →ₗ[A] U) ∘ₗ (↑φ.toLinearEquiv : V →ₗ[A] W)) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g =
    (τ : (a : G) → U →ₗ[A] U) g ∘ₗ (↑ψ.toLinearEquiv : W →ₗ[A] U) ∘ₗ (↑φ.toLinearEquiv : V →ₗ[A] W)
rw₁ :
  (↑ψ.toLinearEquiv : W →ₗ[A] U) ∘ₗ (↑φ.toLinearEquiv : V →ₗ[A] W) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g =
    (τ : (a : G) → U →ₗ[A] U) g ∘ₗ (↑ψ.toLinearEquiv : W →ₗ[A] U) ∘ₗ (↑φ.toLinearEquiv : V →ₗ[A] W)
rw₂ :
  (↑ψ.toLinearEquiv : W →ₗ[A] U) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑φ : ρ.IntertwiningMap σ).toLinearMap =
    (τ : (a : G) → U →ₗ[A] U) g ∘ₗ (↑ψ.toLinearEquiv : W →ₗ[A] U) ∘ₗ (↑φ.toLinearEquiv : V →ₗ[A] W)
rw₃ :
  ((↑ψ.toLinearEquiv : W →ₗ[A] U) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g) ∘ₗ (↑φ : ρ.IntertwiningMap σ).toLinearMap =
    (τ : (a : G) → U →ₗ[A] U) g ∘ₗ (↑ψ.toLinearEquiv : W →ₗ[A] U) ∘ₗ (↑φ.toLinearEquiv : V →ₗ[A] W)
rw₄ :
  Eq (α := V →ₗ[A] U)
    (((τ : (a : G) → U →ₗ[A] U) g ∘ₗ (↑ψ : σ.IntertwiningMap τ).toLinearMap) ∘ₗ (↑φ : ρ.IntertwiningMap σ).toLinearMap)
    ((τ : (a : G) → U →ₗ[A] U) g ∘ₗ (↑ψ.toLinearEquiv : W →ₗ[A] U) ∘ₗ (↑φ.toLinearEquiv : V →ₗ[A] W))
rw₅ rw₆ :
  Eq (α := V →ₗ[A] U)
    ((τ : (a : G) → U →ₗ[A] U) g ∘ₗ (↑ψ : σ.IntertwiningMap τ).toLinearMap ∘ₗ (↑φ : ρ.IntertwiningMap σ).toLinearMap)
    ((τ : (a : G) → U →ₗ[A] U) g ∘ₗ (↑ψ.toLinearEquiv : W →ₗ[A] U) ∘ₗ (↑φ.toLinearEquiv : V →ₗ[A] W))
⊢ (↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv) : V →ₗ[A] U) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g =
    (τ : (a : G) → U →ₗ[A] U) g ∘ₗ (↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv) : V →ₗ[A] U)

Tactic:
rw [LinearEquiv.coe_trans, comp_assoc, φ.1.2, ← comp_assoc, ψ.1.2, comp_assoc]

Premises used: LinearMap.comp_assoc, Representation.IntertwiningMap.isIntertwining', Representation.Equiv.toIntertwiningMap, LinearEquiv.coe_trans
-- 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
φ : ρ.Equiv σ
ψ : σ.Equiv τ
⊢ (↑(φ.trans ψ) : ρ.IntertwiningMap τ) = (↑ψ : σ.IntertwiningMap τ).comp (↑φ : ρ.IntertwiningMap σ)

Tactic:
rfl

Premises used: Representation.IntertwiningMap.comp, 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
φ : ρ.Equiv σ
ψ : σ.Equiv τ
⊢ (↑(φ.trans ψ) : ρ.IntertwiningMap τ).toLinearMap =
    (↑ψ : σ.IntertwiningMap τ).toLinearMap ∘ₗ (↑φ : ρ.IntertwiningMap σ).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
φ : ρ.Equiv σ
ψ : σ.Equiv τ
v : V
⊢ Eq.{u_5 + 1} (α := U) ((φ.trans ψ : (a : V) → U) v : U) ((ψ : (a : W) → U) ((φ : (a : V) → W) v : W) : U)

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
φ : ρ.Equiv σ
v : W
⊢ (φ : (a : V) → W) ((φ.symm : (a : W) → V) v : V) = v

Tactic:
φ.right_inv v

Premises used: Representation.Equiv.right_inv
-- 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
φ : ρ.Equiv σ
v : V
⊢ (φ.symm : (a : W) → V) ((φ : (a : V) → W) v : W) = v

Tactic:
φ.left_inv v

Premises used: Representation.Equiv.left_inv
-- 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
φ : ρ.Equiv σ
h : ∀ (x : V), Eq (α := V) ((φ.trans φ.symm : (a : V) → V) x : V) ((refl ρ : (a : V) → V) x : V)
⊢ φ.trans φ.symm = refl ρ

Tactic:
ext
-- 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
φ : ρ.Equiv σ
x : V
⊢ Eq (α := V) ((φ.trans φ.symm : (a : V) → V) x : V) ((refl ρ : (a : V) → V) x : V)

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
φ : ρ.Equiv σ
h : ∀ (x : W), Eq (α := W) ((φ.symm.trans φ : (a : W) → W) x : W) ((refl σ : (a : W) → W) x : W)
⊢ φ.symm.trans φ = refl σ

Tactic:
ext
-- 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
φ : ρ.Equiv σ
x : W
⊢ Eq (α := W) ((φ.symm.trans φ : (a : W) → W) x : W) ((refl σ : (a : W) → W) x : W)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
g : G
φ : ρ.Equiv σ
h :
  ∀ (w : W),
    Eq (α := W)
      ((((φ.toLinearEquiv.conj : (a : Module.End A V) → Module.End A W) ((ρ : (a : G) → V →ₗ[A] V) g) :
              Module.End A W) :
            (a : W) → W)
          w :
        W)
      ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) w : W)
⊢ Eq.{u_4 + 1} (α := Module.End A W)
    ((φ.toLinearEquiv.conj : (a : Module.End A V) → Module.End A W) ((ρ : (a : G) → V →ₗ[A] V) g) : Module.End A W)
    ((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W)

Tactic:
ext w
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
g : G
φ : ρ.Equiv σ
w : W
⊢ Eq.{u_3 + 1} (α := V)
    (((ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑φ.symm : σ.IntertwiningMap ρ).toLinearMap : (a : W) → V) w : V)
    (((↑φ.symm : σ.IntertwiningMap ρ).toLinearMap ∘ₗ (σ : (a : G) → W →ₗ[A] W) g : (a : W) → V) w : V)

Tactic:
have := (congr($(φ.symm.toIntertwiningMap.2 g) w)).symm
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
g : G
φ : ρ.Equiv σ
w : W
this :
  Eq.{u_3 + 1} (α := V)
    (((ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑φ.symm : σ.IntertwiningMap ρ).toLinearMap : (a : W) → V) w : V)
    (((↑φ.symm : σ.IntertwiningMap ρ).toLinearMap ∘ₗ (σ : (a : G) → W →ₗ[A] W) g : (a : W) → V) w : V)
h :
  Eq.{u_4 + 1} (α := W)
    ((φ : (a : V) → W) ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) ((φ.symm : (a : W) → V) w : V) : V) :
      W)
    ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) w : W)
⊢ Eq (α := W)
    ((((φ.toLinearEquiv.conj : (a : Module.End A V) → Module.End A W) ((ρ : (a : G) → V →ₗ[A] V) g) : Module.End A W) :
          (a : W) → W)
        w :
      W)
    ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) w : W)

Tactic:
simp only [LinearMap.coe_comp, coe_toLinearMap, Function.comp_apply, LinearEquiv.conj_apply_apply,
    coe_symm, toLinearEquiv_apply, coe_toIntertwiningMap] at this ⊢

Premises used: LinearEquiv.conj_apply_apply, Representation.Equiv.coe_toIntertwiningMap, Representation.Equiv.toLinearEquiv_apply, LinearMap.coe_comp, Representation.Equiv.coe_symm, Function.comp_apply, Representation.Equiv.coe_toLinearMap
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
g : G
φ : ρ.Equiv σ
w : W
this :
  Eq (α := V) ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) ((φ.symm : (a : W) → V) w : V) : V)
    ((φ.symm : (a : W) → V) ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) w : W) : V)
⊢ Eq.{u_4 + 1} (α := W)
    ((φ : (a : V) → W) ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) ((φ.symm : (a : W) → V) w : V) : V) :
      W)
    ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) w : W)

Tactic:
simp [this]
-- 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 : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
a : A
f : ρ.IntertwiningMap σ
⊢ ∀ (g : G), (a • f.toLinearMap) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ (a • f.toLinearMap)

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

Premises used: LinearMap.smul_comp, Representation.IntertwiningMap.isIntertwining', LinearMap.comp_smul