awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
φ_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)
⊢ (↑φ.toLinearEquiv.symm : W →ₗ[A] V) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g =
    (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V)
have 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)
Tactic: rw [← cancel_left φ.toLinearEquiv.injective, ← comp_assoc, ← comp_assoc, φ.1.2 g, φ.comp_symm,
      comp_assoc, φ.comp_symm, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
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
⊢ (↑e.symm : W →ₗ[A] V) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g = (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑e.symm : W →ₗ[A] V)
have 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)
Tactic: apply e.comp_toLinearMap_eq_iff _ _ |>.1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
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
⊢ (↑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)
have 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)
Tactic: rw [← comp_assoc, ← comp_assoc, he g, e.comp_symm, id_comp, comp_assoc, e.comp_symm, comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
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)
⊢ (↑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)
have 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)
Tactic: rw [← comp_assoc, ← comp_assoc, he g, e.comp_symm, id_comp, comp_assoc, e.comp_symm, comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
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)
⊢ (↑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)
have 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)
Tactic: rw [← comp_assoc, ← comp_assoc, he g, e.comp_symm, id_comp, comp_assoc, e.comp_symm, comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
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)
⊢ (↑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)
have 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))
Tactic: rw [← comp_assoc, ← comp_assoc, he g, e.comp_symm, id_comp, comp_assoc, e.comp_symm, comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
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))
⊢ (↑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)
have 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)
Tactic: rw [← comp_assoc, ← comp_assoc, he g, e.comp_symm, id_comp, comp_assoc, e.comp_symm, comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
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)
⊢ (↑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)
have 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)
Tactic: rw [← comp_assoc, ← comp_assoc, he g, e.comp_symm, id_comp, comp_assoc, e.comp_symm, comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
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)
⊢ (↑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)
have 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)
Tactic: rw [← comp_assoc, ← comp_assoc, he g, e.comp_symm, id_comp, comp_assoc, e.comp_symm, comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
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)
⊢ (↑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)
have 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)
Tactic: rw [← comp_assoc, ← comp_assoc, he g, e.comp_symm, id_comp, comp_assoc, e.comp_symm, comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
φ_1 φ : ρ.Equiv σ
ψ : σ.Equiv τ
g : G
⊢ (↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv) : V →ₗ[A] U) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g =
    (τ : (a : G) → U →ₗ[A] U) g ∘ₗ (↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv) : V →ₗ[A] U)
have 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)
Tactic: rw [LinearEquiv.coe_trans, comp_assoc, φ.1.2, ← comp_assoc, ψ.1.2, comp_assoc]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : 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)
⊢ (↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv) : V →ₗ[A] U) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g =
    (τ : (a : G) → U →ₗ[A] U) g ∘ₗ (↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv) : V →ₗ[A] U)
have 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)
Tactic: rw [LinearEquiv.coe_trans, comp_assoc, φ.1.2, ← comp_assoc, ψ.1.2, comp_assoc]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : 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)
⊢ (↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv) : V →ₗ[A] U) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g =
    (τ : (a : G) → U →ₗ[A] U) g ∘ₗ (↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv) : V →ₗ[A] U)
have 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)
Tactic: rw [LinearEquiv.coe_trans, comp_assoc, φ.1.2, ← comp_assoc, ψ.1.2, comp_assoc]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : 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)
⊢ (↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv) : V →ₗ[A] U) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g =
    (τ : (a : G) → U →ₗ[A] U) g ∘ₗ (↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv) : V →ₗ[A] U)
have 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)
Tactic: rw [LinearEquiv.coe_trans, comp_assoc, φ.1.2, ← comp_assoc, ψ.1.2, comp_assoc]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : 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)
⊢ (↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv) : V →ₗ[A] U) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g =
    (τ : (a : G) → U →ₗ[A] U) g ∘ₗ (↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv) : V →ₗ[A] U)
have 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))
Tactic: rw [LinearEquiv.coe_trans, comp_assoc, φ.1.2, ← comp_assoc, ψ.1.2, comp_assoc]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : 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))
⊢ (↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv) : V →ₗ[A] U) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g =
    (τ : (a : G) → U →ₗ[A] U) g ∘ₗ (↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv) : V →ₗ[A] U)
have 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))
Tactic: rw [LinearEquiv.coe_trans, comp_assoc, φ.1.2, ← comp_assoc, ψ.1.2, comp_assoc]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
φ : ρ.Equiv σ
⊢ φ.trans φ.symm = refl ρ
have h : ∀ (x : V), Eq (α := V) ((φ.trans φ.symm : (a : V) → V) x : V) ((refl ρ : (a : V) → V) x : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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.trans φ = refl σ
have h : ∀ (x : W), Eq (α := W) ((φ.symm.trans φ : (a : W) → W) x : W) ((refl σ : (a : W) → W) x : W)
Tactic: ext