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₁ f₂ : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
⊢ (f₁ + f₂).comp g = f₁.comp g + f₂.comp g
have h : ((f₁ + f₂).comp g).toLinearMap = (f₁.comp g + f₂.comp g).toLinearMap
Tactic: ext1
-- 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 : σ.IntertwiningMap τ
g₁ g₂ : ρ.IntertwiningMap σ
⊢ f.comp (g₁ + g₂) = f.comp g₁ + f.comp g₂
have h : (f.comp (g₁ + g₂)).toLinearMap = (f.comp g₁ + f.comp g₂).toLinearMap
Tactic: ext1
-- 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 ρ
h : φ.toLinearEquiv = ψ.toLinearEquiv
⊢ φ = ψ
have mk' : ∀ (toIntertwiningMap : σ.IntertwiningMap ρ) (invFun : V → W)
  (left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun)
  (right_inv : Function.RightInverse invFun toIntertwiningMap.toFun)
  (h :
    { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
          σ.Equiv ρ }.toLinearEquiv =
      ψ.toLinearEquiv),
  { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
      σ.Equiv ρ } =
    ψ
Tactic: cases φ
Cleared hypotheses: φ, h
-- 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 ρ
toIntertwiningMap : σ.IntertwiningMap ρ
invFun : V → W
left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun
right_inv : Function.RightInverse invFun toIntertwiningMap.toFun
h :
  { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
        σ.Equiv ρ }.toLinearEquiv =
    ψ.toLinearEquiv
⊢ { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
      σ.Equiv ρ } =
    ψ
have mk' : ∀ (toIntertwiningMap_1 : σ.IntertwiningMap ρ) (invFun_1 : V → W)
  (left_inv_1 : Function.LeftInverse invFun_1 toIntertwiningMap_1.toFun)
  (right_inv_1 : Function.RightInverse invFun_1 toIntertwiningMap_1.toFun)
  (h :
    { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
          σ.Equiv ρ }.toLinearEquiv =
      { toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 :
          σ.Equiv ρ }.toLinearEquiv),
  { 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: cases ψ
Cleared hypotheses: ψ, h
-- 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 σ
h1 : Eq (α := V → W) (⇑φ.toLinearEquiv : (a : V) → W) (⇑ψ.toLinearEquiv : (a : V) → W)
h2 : φ.invFun = ψ.invFun
⊢ φ = ψ
have mk' : ∀ (toIntertwiningMap : ρ.IntertwiningMap σ) (invFun : W → V)
  (left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun)
  (right_inv : Function.RightInverse invFun toIntertwiningMap.toFun)
  (h1 :
    Eq (α := V → W)
      (⇑{ toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
              ρ.Equiv σ }.toLinearEquiv :
        (a : V) → W)
      (⇑ψ.toLinearEquiv : (a : V) → W))
  (h2 :
    { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
          ρ.Equiv σ }.invFun =
      ψ.invFun),
  { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
      ρ.Equiv σ } =
    ψ
Tactic: cases φ
Cleared hypotheses: φ, h1, h2
-- 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
φ ψ : ρ.Equiv σ
toIntertwiningMap : ρ.IntertwiningMap σ
invFun : W → V
left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun
right_inv : Function.RightInverse invFun toIntertwiningMap.toFun
h1 :
  Eq (α := V → W)
    (⇑{ toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
            ρ.Equiv σ }.toLinearEquiv :
      (a : V) → W)
    (⇑ψ.toLinearEquiv : (a : V) → W)
h2 :
  { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
        ρ.Equiv σ }.invFun =
    ψ.invFun
⊢ { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
      ρ.Equiv σ } =
    ψ
have 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)
  (h1 :
    Eq (α := V → W)
      (⇑{ toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
              ρ.Equiv σ }.toLinearEquiv :
        (a : V) → W)
      (⇑{ toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1,
              right_inv := right_inv_1 : ρ.Equiv σ }.toLinearEquiv :
        (a : V) → W))
  (h2 :
    { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
          ρ.Equiv σ }.invFun =
      { toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 :
          ρ.Equiv σ }.invFun),
  { 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: cases ψ
Cleared hypotheses: ψ, h1, h2
-- 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 σ
h : Eq (α := (a : V) → W) (⇑φ : (a : V) → W) (⇑ψ : (a : V) → W)
⊢ φ = ψ
have mk' : ∀ (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)),
  { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
      ρ.Equiv σ } =
    ψ
Tactic: cases φ
Cleared hypotheses: φ, h
-- 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 σ
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)
⊢ { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
      ρ.Equiv σ } =
    ψ
have 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 }
Tactic: cases ψ
Cleared hypotheses: ψ, h
-- 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
⊢ (↑φ.toLinearEquiv.symm : W →ₗ[A] V) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g =
    (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V)
have 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)
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
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)
⊢ (↑φ.toLinearEquiv.symm : W →ₗ[A] V) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g =
    (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V)
have 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)
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
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)
⊢ (↑φ.toLinearEquiv.symm : W →ₗ[A] V) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g =
    (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V)
have 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)
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
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)
⊢ (↑φ.toLinearEquiv.symm : W →ₗ[A] V) ∘ₗ (σ : (a : G) → W →ₗ[A] W) g =
    (ρ : (a : G) → V →ₗ[A] V) g ∘ₗ (↑φ.toLinearEquiv.symm : W →ₗ[A] V)
have 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)
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
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)
⊢ (↑φ.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 (α := W →ₗ[A] W) (LinearMap.id ∘ₗ (σ : (a : G) → W →ₗ[A] W) g)
  (((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑φ : ρ.IntertwiningMap σ).toLinearMap) ∘ₗ (↑φ.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]
-- 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))
⊢ (↑φ.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 (α := W →ₗ[A] W) (LinearMap.id ∘ₗ (σ : (a : G) → W →ₗ[A] W) g)
  ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑φ : ρ.IntertwiningMap σ).toLinearMap ∘ₗ (↑φ.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]
-- 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))
⊢ (↑φ.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) (LinearMap.id ∘ₗ (σ : (a : G) → W →ₗ[A] W) g)
  ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ LinearMap.id)
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
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)
⊢ (↑φ.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 ∘ₗ LinearMap.id : 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]