awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
X Y : Rep.{w, u, v} k G
f : (↑X : Type w) →ₗ[k] (↑Y : Type w)
g : G
h :
  (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
⊢ Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    (((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
        f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
have mp : Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
    (f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
Tactic: rw [LinearMap.comp_assoc, LinearMap.comp_assoc, ← Rep.ρ_mul, inv_mul_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
X Y : Rep.{w, u, v} k G
f : (↑X : Type w) →ₗ[k] (↑Y : Type w)
g : G
h :
  (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mp :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      (f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹) ∘ₗ
        (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
⊢ Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    (((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
        f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
have mp₁ : Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
    f ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
Tactic: rw [LinearMap.comp_assoc, LinearMap.comp_assoc, ← Rep.ρ_mul, inv_mul_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
X Y : Rep.{w, u, v} k G
f : (↑X : Type w) →ₗ[k] (↑Y : Type w)
g : G
h :
  (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mp :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      (f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹) ∘ₗ
        (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
mp₁ :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ
        (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ ∘ₗ
          (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
⊢ Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    (((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
        f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
have mp₂ : Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
    f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) (g⁻¹ * g))
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
Tactic: rw [LinearMap.comp_assoc, LinearMap.comp_assoc, ← Rep.ρ_mul, inv_mul_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
X Y : Rep.{w, u, v} k G
f : (↑X : Type w) →ₗ[k] (↑Y : Type w)
g : G
h :
  (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mp :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      (f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹) ∘ₗ
        (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
mp₁ :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ
        (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ ∘ₗ
          (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
mp₂ :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) (g⁻¹ * g))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
⊢ Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    (((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
        f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
have mp₃ : Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) 1)
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
Tactic: rw [LinearMap.comp_assoc, LinearMap.comp_assoc, ← Rep.ρ_mul, inv_mul_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
X Y : Rep.{w, u, v} k G
f : (↑X : Type w) →ₗ[k] (↑Y : Type w)
g : G
h :
  (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mp :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      (f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹) ∘ₗ
        (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
mp₁ :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ
        (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ ∘ₗ
          (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
mp₂ :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) (g⁻¹ * g))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
mp₃ :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) 1)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
⊢ Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    (((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
        f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
have mp₄ : Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w)) ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f ∘ₗ 1)
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
Tactic: rw [LinearMap.comp_assoc, LinearMap.comp_assoc, ← Rep.ρ_mul, inv_mul_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
X Y : Rep.{w, u, v} k G
f : (↑X : Type w) →ₗ[k] (↑Y : Type w)
g : G
h :
  (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mp :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      (f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹) ∘ₗ
        (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
mp₁ :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ
        (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ ∘ₗ
          (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
mp₂ :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) (g⁻¹ * g))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
mp₃ :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) 1)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
mp₄ :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w)) ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f ∘ₗ 1)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
⊢ Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    (((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
        f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
have mp₅ : Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w)) ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f ∘ₗ LinearMap.id)
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
Tactic: rw [LinearMap.comp_assoc, LinearMap.comp_assoc, ← Rep.ρ_mul, inv_mul_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
X Y : Rep.{w, u, v} k G
f : (↑X : Type w) →ₗ[k] (↑Y : Type w)
g : G
h :
  (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mp :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      (f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹) ∘ₗ
        (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
mp₁ :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ
        (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ ∘ₗ
          (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
mp₂ :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) (g⁻¹ * g))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
mp₃ :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) 1)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
mp₄ :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w)) ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f ∘ₗ 1)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
mp₅ :
  Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f ∘ₗ LinearMap.id)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
⊢ Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w))
    (((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
        f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g)
    ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
have mp₆ : Eq (α := (↑X : Type w) →ₗ[k] (↑Y : Type w)) ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f)
Tactic: rw [LinearMap.comp_assoc, LinearMap.comp_assoc, ← Rep.ρ_mul, inv_mul_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
X Y : Rep.{w, u, v} k G
f : (↑X : Type w) →ₗ[k] (↑Y : Type w)
g : G
h :
  f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g =
    (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f
⊢ (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
have mpr : ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f) ∘ₗ
    (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
  f
Tactic: rw [← LinearMap.comp_assoc, ← h, LinearMap.comp_assoc, ← Rep.ρ_mul, mul_inv_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
X Y : Rep.{w, u, v} k G
f : (↑X : Type w) →ₗ[k] (↑Y : Type w)
g : G
h :
  f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g =
    (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f
mpr :
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
⊢ (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
have mpr₁ : (f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g) ∘ₗ
    (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
  f
Tactic: rw [← LinearMap.comp_assoc, ← h, LinearMap.comp_assoc, ← Rep.ρ_mul, mul_inv_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
X Y : Rep.{w, u, v} k G
f : (↑X : Type w) →ₗ[k] (↑Y : Type w)
g : G
h :
  f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g =
    (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f
mpr :
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mpr₁ :
  (f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
⊢ (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
have mpr₂ : f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
  f
Tactic: rw [← LinearMap.comp_assoc, ← h, LinearMap.comp_assoc, ← Rep.ρ_mul, mul_inv_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
X Y : Rep.{w, u, v} k G
f : (↑X : Type w) →ₗ[k] (↑Y : Type w)
g : G
h :
  f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g =
    (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f
mpr :
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mpr₁ :
  (f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mpr₂ :
  f ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
⊢ (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
have mpr₃ : f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) (g * g⁻¹) = f
Tactic: rw [← LinearMap.comp_assoc, ← h, LinearMap.comp_assoc, ← Rep.ρ_mul, mul_inv_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
X Y : Rep.{w, u, v} k G
f : (↑X : Type w) →ₗ[k] (↑Y : Type w)
g : G
h :
  f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g =
    (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f
mpr :
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mpr₁ :
  (f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mpr₂ :
  f ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mpr₃ : f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) (g * g⁻¹) = f
⊢ (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
have mpr₄ : f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) 1 = f
Tactic: rw [← LinearMap.comp_assoc, ← h, LinearMap.comp_assoc, ← Rep.ρ_mul, mul_inv_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
X Y : Rep.{w, u, v} k G
f : (↑X : Type w) →ₗ[k] (↑Y : Type w)
g : G
h :
  f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g =
    (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f
mpr :
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mpr₁ :
  (f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mpr₂ :
  f ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mpr₃ : f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) (g * g⁻¹) = f
mpr₄ : f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) 1 = f
⊢ (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
have mpr₅ : f ∘ₗ 1 = f
Tactic: rw [← LinearMap.comp_assoc, ← h, LinearMap.comp_assoc, ← Rep.ρ_mul, mul_inv_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
X Y : Rep.{w, u, v} k G
f : (↑X : Type w) →ₗ[k] (↑Y : Type w)
g : G
h :
  f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g =
    (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f
mpr :
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mpr₁ :
  (f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mpr₂ :
  f ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mpr₃ : f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) (g * g⁻¹) = f
mpr₄ : f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) 1 = f
mpr₅ : f ∘ₗ 1 = f
⊢ (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
have mpr₆ : f ∘ₗ LinearMap.id = f
Tactic: rw [← LinearMap.comp_assoc, ← h, LinearMap.comp_assoc, ← Rep.ρ_mul, mul_inv_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
X Y : Rep.{w, u, v} k G
f : (↑X : Type w) →ₗ[k] (↑Y : Type w)
g : G
h :
  f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g =
    (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f
mpr :
  ((Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mpr₁ :
  (f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g) ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mpr₂ :
  f ∘ₗ
      (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
mpr₃ : f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) (g * g⁻¹) = f
mpr₄ : f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) 1 = f
mpr₅ : f ∘ₗ 1 = f
mpr₆ : f ∘ₗ LinearMap.id = f
⊢ (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
      f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
    f
have mpr₇ : f = f
Tactic: rw [← LinearMap.comp_assoc, ← h, LinearMap.comp_assoc, ← Rep.ρ_mul, mul_inv_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
X Y : FDRep k G
⊢ ↥(linHom X.ρ Y.ρ).invariants ≃ₗ[k] X ⟶ Y
have rw : ↥((Functor.obj
              (forget₂ (FDRep k G) (FC :=
                HomSubtype (FGModuleCat k) G (FV :=
                  fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat k) (ModuleCat.isFG k)) ↦
                  (↑(X.obj (P := ModuleCat.isFG k)) : Type u) →ₗ[k] (↑(Y.obj (P := ModuleCat.isFG k)) : Type u)) (CV :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat k) (ModuleCat.isFG k)) ↦
                  (↑(X.obj (P := ModuleCat.isFG k)) : Type u)))
                (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat k) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG k)) : Type u))
                (Rep k G) (FD := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
              X).ρ.linHom
        (Functor.obj
            (forget₂ (FDRep k G) (FC :=
              HomSubtype (FGModuleCat k) G (FV :=
                fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat k) (ModuleCat.isFG k)) ↦
                (↑(X.obj (P := ModuleCat.isFG k)) : Type u) →ₗ[k] (↑(Y.obj (P := ModuleCat.isFG k)) : Type u)) (CV :=
                fun (X : ObjectProperty.FullSubcategory (C := ModuleCat k) (ModuleCat.isFG k)) ↦
                (↑(X.obj (P := ModuleCat.isFG k)) : Type u)))
              (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat k) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG k)) : Type u))
              (Rep k G) (FD := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
            Y).ρ).invariants ≃ₗ[k]
  X ⟶ Y
Tactic: rw [← FDRep.forget₂_ρ, ← FDRep.forget₂_ρ]