awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
x : V
⊢ x ∈ ρ.invariants.carrier ↔
    Membership.mem (γ := Set V)
      (⋂ (g : G), Function.fixedPoints (⇑((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V)) x

Tactic:
simp [Function.IsFixedPt]

Premises used: Function.IsFixedPt
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
inst_4 : ρ.IsTrivial
⊢ ρ.invariants = ⊤

Tactic:
eq_top_iff.2 (fun x _ g => ρ.isTrivial_apply g x)

Premises used: Iff.mpr, eq_top_iff, Representation.isTrivial_apply
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : V
hx : (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x = x
γ : G
rcases : ∀ (i : ℤ), ((ρ : (a : G) → V →ₗ[k] V) ((fun (x : ℤ) ↦ g ^ x) i) : (a : V) → V) x = x
⊢ (((ρ : (a : G) → V →ₗ[k] V) γ : V →ₗ[k] V) : (a : V) → V) x = x

Tactic:
rcases hg γ with ⟨i, rfl⟩

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : V
hx : (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x = x
⊢ ((ρ : (a : G) → V →ₗ[k] V) ((fun (x : ℤ) ↦ g ^ x) 0) : (a : V) → V) x = x

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : V
hx : (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x = x
i : ℕ
h : ((ρ : (a : G) → V →ₗ[k] V) ((fun (x : ℤ) ↦ g ^ x) (↑i : ℤ)) : (a : V) → V) x = x
⊢ ((ρ : (a : G) → V →ₗ[k] V) ((fun (x : ℤ) ↦ g ^ x) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)) : (a : V) → V) x = x

Tactic:
simp_all [zpow_add_one]

Premises used: zpow_add_one
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : V
hx : (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x = x
i : ℕ
h : ((ρ : (a : G) → V →ₗ[k] V) ((fun (x : ℤ) ↦ g ^ x) (-(↑i : ℤ))) : (a : V) → V) x = x
⊢ ((ρ : (a : G) → V →ₗ[k] V) ((fun (x : ℤ) ↦ g ^ x) (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)) : (a : V) → V) x = x

Tactic:
_
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : V
hx : (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x = x
i : ℤ
pred :
  ∀ (i : ℕ) (h : ((ρ : (a : G) → V →ₗ[k] V) ((fun (x : ℤ) ↦ g ^ x) (-(↑i : ℤ))) : (a : V) → V) x = x),
    ((ρ : (a : G) → V →ₗ[k] V) ((fun (x : ℤ) ↦ g ^ x) (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)) : (a : V) → V) x = x
⊢ ((ρ : (a : G) → V →ₗ[k] V) ((fun (x : ℤ) ↦ g ^ x) i) : (a : V) → V) x = x

Tactic:
induction i with | zero => simp | succ i _ => simp_all [zpow_add_one] | pred i h => _

Premises used: zpow_add_one
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : V
hx : (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x = x
i : ℕ
h : ((ρ : (a : G) → V →ₗ[k] V) ((fun (x : ℤ) ↦ g ^ x) (-(↑i : ℤ))) : (a : V) → V) x = x
⊢ ((ρ : (a : G) → V →ₗ[k] V) ((fun (x : ℤ) ↦ g ^ x) (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)) : (a : V) → V) x = x

Tactic:
simpa [neg_sub_comm _ (1 : ℤ), zpow_sub] using congr(ρ g⁻¹ $(h.trans hx.symm))

Premises used: neg_sub_comm, OfNat.ofNat, zpow_sub
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
ρ : Representation k G V
σ : Representation k G W
f : V →ₗ[k] W
⊢ (∀ (g : G), (σ : (a : G) → W →ₗ[k] W) g ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g⁻¹ = f) ↔ ρ.IsIntertwiningMap σ f

Tactic:
⟨fun hf ↦ ⟨fun γ v ↦ ?_⟩, fun hf γ ↦ ?_⟩

Premises used: Iff.intro, Representation.IsIntertwiningMap.mk
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
ρ : Representation k G V
σ : Representation k G W
f : V →ₗ[k] W
refine_1 :
  ∀ (hf : ∀ (g : G), (σ : (a : G) → W →ₗ[k] W) g ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g⁻¹ = f) (γ : G) (v : V),
    Eq (α := W) ((f : (a : V) → W) ((((ρ : (a : G) → V →ₗ[k] V) γ : V →ₗ[k] V) : (a : V) → V) v : V) : W)
      ((((σ : (a : G) → W →ₗ[k] W) γ : W →ₗ[k] W) : (a : W) → W) ((f : (a : V) → W) v : W) : W)
refine_2 :
  ∀ (hf : ρ.IsIntertwiningMap σ f) (γ : G), (σ : (a : G) → W →ₗ[k] W) γ ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) γ⁻¹ = f
⊢ (∀ (g : G), (σ : (a : G) → W →ₗ[k] W) g ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g⁻¹ = f) ↔ ρ.IsIntertwiningMap σ f

Tactic:
refine ⟨fun hf ↦ ⟨fun γ v ↦ ?_⟩, fun hf γ ↦ ?_⟩
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
ρ : Representation k G V
σ : Representation k G W
f : V →ₗ[k] W
hf : ∀ (g : G), (σ : (a : G) → W →ₗ[k] W) g ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g⁻¹ = f
γ : G
v : V
⊢ (σ : (a : G) → W →ₗ[k] W) γ ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) γ⁻¹ = f

Tactic:
specialize hf γ
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
ρ : Representation k G V
σ : Representation k G W
f : V →ₗ[k] W
γ : G
v : V
hf : (σ : (a : G) → W →ₗ[k] W) γ ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) γ⁻¹ = f
refine_1 :
  Eq (α := W)
    (((σ : (a : G) → W →ₗ[k] W) γ ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) γ⁻¹ : (a : V) → W)
        ((((ρ : (a : G) → V →ₗ[k] V) γ : V →ₗ[k] V) : (a : V) → V) v : V) :
      W)
    ((((σ : (a : G) → W →ₗ[k] W) γ : W →ₗ[k] W) : (a : W) → W) ((f : (a : V) → W) v : W) : W)
⊢ Eq (α := W) ((f : (a : V) → W) ((((ρ : (a : G) → V →ₗ[k] V) γ : V →ₗ[k] V) : (a : V) → V) v : V) : W)
    ((((σ : (a : G) → W →ₗ[k] W) γ : W →ₗ[k] W) : (a : W) → W) ((f : (a : V) → W) v : W) : W)

Tactic:
nth_rewrite 1 [← hf]
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
ρ : Representation k G V
σ : Representation k G W
f : V →ₗ[k] W
γ : G
v : V
hf : (σ : (a : G) → W →ₗ[k] W) γ ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) γ⁻¹ = f
⊢ Eq (α := W)
    (((σ : (a : G) → W →ₗ[k] W) γ ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) γ⁻¹ : (a : V) → W)
        ((((ρ : (a : G) → V →ₗ[k] V) γ : V →ₗ[k] V) : (a : V) → V) v : V) :
      W)
    ((((σ : (a : G) → W →ₗ[k] W) γ : W →ₗ[k] W) : (a : W) → W) ((f : (a : V) → W) v : W) : W)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
ρ : Representation k G V
σ : Representation k G W
f : V →ₗ[k] W
hf : ρ.IsIntertwiningMap σ f
γ : G
refine_2 :
  ∀ (v : V),
    Eq.{u_4 + 1} (α := W) (((σ : (a : G) → W →ₗ[k] W) γ ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) γ⁻¹ : (a : V) → W) v : W)
      ((f : (a : V) → W) v : W)
⊢ (σ : (a : G) → W →ₗ[k] W) γ ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) γ⁻¹ = f

Tactic:
ext v
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
ρ : Representation k G V
σ : Representation k G W
f : V →ₗ[k] W
hf : ρ.IsIntertwiningMap σ f
γ : G
v : V
⊢ Eq.{u_4 + 1} (α := W) (((σ : (a : G) → W →ₗ[k] W) γ ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) γ⁻¹ : (a : V) → W) v : W)
    ((f : (a : V) → W) v : W)

Tactic:
simp [hf.isIntertwining]

Premises used: Representation.IsIntertwiningMap.isIntertwining
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
inst_4 : Fintype G
inst_5 : Invertible (α := k) (↑(Fintype.card G) : k)
v : V
g : G
rw :
  Eq (α := V)
    ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V)
        ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (average k G) : Module.End k V) : (a : V) → V) v : V) :
      V)
    ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (average k G) : Module.End k V) : (a : V) → V) v : V)
rw₁ :
  Eq (α := V)
    ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (single g 1) : Module.End k V) : (a : V) → V)
        ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (average k G) : Module.End k V) : (a : V) → V) v : V) :
      V)
    ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (average k G) : Module.End k V) : (a : V) → V) v : V)
rw₂ :
  Eq (α := V)
    ((HMul.hMul (α := Module.End k V) (β := Module.End k V)
            ((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (single g 1) : Module.End k V)
            ((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (average k G) : Module.End k V) :
          (a : V) → V)
        v :
      V)
    ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (average k G) : Module.End k V) : (a : V) → V) v : V)
rw₃ :
  Eq (α := V)
    ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (HMul.hMul (α := k[G]) (single g 1) (average k G)) :
            Module.End k V) :
          (a : V) → V)
        v :
      V)
    ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (average k G) : Module.End k V) : (a : V) → V) v : V)
rw₄ rw₅ :
  Eq (α := V) ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (average k G) : Module.End k V) : (a : V) → V) v : V)
    ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (average k G) : Module.End k V) : (a : V) → V) v : V)
⊢ Eq (α := V) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) ((ρ.averageMap : (a : V) → V) v : V) : V)
    ((ρ.averageMap : (a : V) → V) v : V)

Tactic:
rw [averageMap, ← asAlgebraHom_single_one, ← Module.End.mul_apply, ← map_mul (asAlgebraHom ρ),
    mul_average_left]

Premises used: Representation.asAlgebraHom, Representation.asAlgebraHom_single_one, map_mul, Representation.averageMap, GroupAlgebra.mul_average_left, Module.End.mul_apply
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
inst_4 : Fintype G
inst_5 : Invertible (α := k) (↑(Fintype.card G) : k)
v : V
hv : v ∈ ρ.invariants
⊢ ∀ (g : G), (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v = v

Tactic:
rw [mem_invariants] at hv

Premises used: Representation.mem_invariants
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
inst_4 : Fintype G
inst_5 : Invertible (α := k) (↑(Fintype.card G) : k)
v : V
hv : ∀ (g : G), (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v = v
⊢ (ρ.averageMap : (a : V) → V) v = v

Tactic:
simp [average, map_sum, hv, Finset.card_univ, ← Nat.cast_smul_eq_nsmul k _ v, smul_smul]

Premises used: Finset.card_univ, GroupAlgebra.average, smul_smul, map_sum, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
inst_4 : Fintype G
inst_5 : Invertible (α := k) (↑(Fintype.card G) : k)
⊢ LinearMap.IsProj ρ.invariants ρ.averageMap

Tactic:
⟨ρ.averageMap_invariant, ρ.averageMap_id⟩

Premises used: LinearMap.IsProj.mk, Representation.averageMap_invariant, Representation.averageMap_id
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
V : Type u_5
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_4 : S.Normal
g : G
x : V
hx : x ∈ invariants (MonoidHom.comp ρ S.subtype)
x_1 : ↥S
s : G
hs : s ∈ S
⊢ Eq (α := V)
    ((((MonoidHom.comp ρ S.subtype : (a : ↥S) → V →ₗ[k] V) (Subtype.mk (p := fun (x : G) ↦ x ∈ S) s hs) : V →ₗ[k] V) :
          (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V) :
      V)
    ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V)

Tactic:
simpa using congr(ρ g $(hx ⟨(g⁻¹ * s * g), Subgroup.Normal.conj_mem' ‹_› s hs g⟩))
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u_1
G : Type u_2
V_1 : Type u_3
W : Type u_4
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup V_1
inst_3 : Module k V_1
inst_4 : AddCommGroup W
inst_5 : Module k W
ρ_1 : Representation k G V_1
σ : Representation k G W
V : Type u_5
inst_6 : AddCommGroup V
inst_7 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_8 : S.Normal
g : ↥S
x_1 : ↥(invariants (MonoidHom.comp ρ S.subtype))
x : V
hx : x ∈ invariants (MonoidHom.comp ρ S.subtype)
⊢ Eq.{u_5 + 1} (α := V)
    (↑((((MonoidHom.comp (ρ.toInvariants S) S.subtype :
                  (a : ↥S) →
                    ↥(invariants (MonoidHom.comp ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp ρ S.subtype)))
                g :
              ↥(invariants (MonoidHom.comp ρ S.subtype)) →ₗ[k] ↥(invariants (MonoidHom.comp ρ S.subtype))) :
            (a : ↥(invariants (MonoidHom.comp ρ S.subtype))) → ↥(invariants (MonoidHom.comp ρ S.subtype)))
          (Subtype.mk (p := fun (x : V) ↦ x ∈ invariants (MonoidHom.comp ρ S.subtype)) x hx)) :
      V)
    (↑((LinearMap.id : (a : ↥(invariants (MonoidHom.comp ρ S.subtype))) → ↥(invariants (MonoidHom.comp ρ S.subtype)))
          (Subtype.mk (p := fun (x : V) ↦ x ∈ invariants (MonoidHom.comp ρ S.subtype)) x hx)) :
      V)

Tactic:
simpa using (hx g)
-- Module: Mathlib.RepresentationTheory.Invariants
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
dsimp :
  (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
        f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
      f ↔
    f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g =
      (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f
⊢ (((X.ρ.linHom Y.ρ : (a : G) → ((↑X : Type w) →ₗ[k] (↑Y : Type w)) →ₗ[k] (↑X : Type w) →ₗ[k] (↑Y : Type w)) g :
            ((↑X : Type w) →ₗ[k] (↑Y : Type w)) →ₗ[k] (↑X : Type w) →ₗ[k] (↑Y : Type w)) :
          (a : (↑X : Type w) →ₗ[k] (↑Y : Type w)) → (↑X : Type w) →ₗ[k] (↑Y : Type w))
        f =
      f ↔
    f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g =
      (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f

Tactic:
dsimp
-- Module: Mathlib.RepresentationTheory.Invariants
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
mp :
  (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
        f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
      f →
    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 :
  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
⊢ (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ
        f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g⁻¹ =
      f ↔
    f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g =
      (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f

Tactic:
constructor
-- Module: Mathlib.RepresentationTheory.Invariants
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)
⊢ f ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g =
    (Y.ρ : (a : G) → (↑Y : Type w) →ₗ[k] (↑Y : Type w)) g ∘ₗ f

Tactic:
nth_rw 1 [← h]
-- Module: Mathlib.RepresentationTheory.Invariants
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)
mp₆ 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)
⊢ 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]

Premises used: inv_mul_cancel, Module.End.one_eq_id, LinearMap.comp_assoc, Rep.ρ_mul, map_one, LinearMap.comp_id
-- Module: Mathlib.RepresentationTheory.Invariants
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
mpr₇ mpr₈ : f = 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

Tactic:
rw [← LinearMap.comp_assoc, ← h, LinearMap.comp_assoc, ← Rep.ρ_mul, mul_inv_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]

Premises used: Module.End.one_eq_id, LinearMap.comp_assoc, Rep.ρ_mul, map_one, mul_inv_cancel, LinearMap.comp_id
-- Module: Mathlib.RepresentationTheory.Invariants
Goal:
k : Type u
inst : Field k
G : Type v
inst_1 : Group G
X Y : FDRep k G
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
⊢ ↥(linHom X.ρ Y.ρ).invariants ≃ₗ[k] X ⟶ Y

Tactic:
rw [← FDRep.forget₂_ρ, ← FDRep.forget₂_ρ]

Premises used: FDRep.forget₂_ρ