awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
⊢ HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, single (g * x) 1) =
    HSMul.hSMul (α := k) (β := k[G])
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _) (∑ x : G, single x 1)
have set : let f : G → k[G] := fun (x : G) ↦ Finsupp.single x 1;
HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ x : G, single (g * x) 1) =
  HSMul.hSMul (α := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (Finset.sum Finset.univ f)
Tactic: set f : G → k[G] := fun x => Finsupp.single x 1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
f : G → k[G] := fun (x : G) ↦ Finsupp.single x 1
⊢ HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, single (g * x) 1) =
    HSMul.hSMul (α := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (Finset.sum Finset.univ f)
have change : HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ x : G, f (g * x)) =
  HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ x : G, f x)
Tactic: change ⅟(Fintype.card G : k) • ∑ x : G, f (g * x) = ⅟(Fintype.card G : k) • ∑ x : G, f x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
f : G → k[G] := fun (x : G) ↦ Finsupp.single x 1
⊢ HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, f (g * x)) =
    HSMul.hSMul (α := k) (β := k[G])
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _) (∑ x : G, f x)
have rw : HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ i : G, f i) =
  HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ x : G, f x)
Tactic: rw [Function.Bijective.sum_comp (Group.mulLeft_bijective g) _]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
⊢ HMul.hMul (α := k[G]) (average k G) (Finsupp.single g 1) = average k G
have simp : HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ x : G, single (x * g) 1) =
  HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ x : G, single x 1)
Tactic: simp only [mul_one, Finset.sum_mul, Algebra.smul_mul_assoc, average, MonoidAlgebra.of_apply,
    MonoidAlgebra.single_mul_single]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
⊢ HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, single (x * g) 1) =
    HSMul.hSMul (α := k) (β := k[G])
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _) (∑ x : G, single x 1)
have set : let f : G → k[G] := fun (x : G) ↦ Finsupp.single x 1;
HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ x : G, single (x * g) 1) =
  HSMul.hSMul (α := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (Finset.sum Finset.univ f)
Tactic: set f : G → k[G] := fun x => Finsupp.single x 1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
f : G → k[G] := fun (x : G) ↦ Finsupp.single x 1
⊢ HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, single (x * g) 1) =
    HSMul.hSMul (α := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (Finset.sum Finset.univ f)
have change : HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ x : G, f (x * g)) =
  HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ x : G, f x)
Tactic: change ⅟(Fintype.card G : k) • ∑ x : G, f (x * g) = ⅟(Fintype.card G : k) • ∑ x : G, f x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : Invertible (α := k) (↑(Fintype.card G) : k)
g : G
f : G → k[G] := fun (x : G) ↦ Finsupp.single x 1
⊢ HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ x : G, f (x * g)) =
    HSMul.hSMul (α := k) (β := k[G])
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _) (∑ x : G, f x)
have rw : HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ i : G, f i) =
  HSMul.hSMul (α := k) (β := k[G]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
    (∑ x : G, f x)
Tactic: rw [Function.Bijective.sum_comp (Group.mulRight_bijective g) _]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
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
⊢ ρ.invariants.carrier = ⋂ (g : G), Function.fixedPoints (⇑((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V)
have h : ∀ (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: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
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
⊢ (((ρ : (a : G) → V →ₗ[k] V) γ : V →ₗ[k] V) : (a : V) → V) x = x
have rcases : ∀ (i : ℤ), ((ρ : (a : G) → V →ₗ[k] V) ((fun (x : ℤ) ↦ g ^ x) i) : (a : V) → V) x = x
Tactic: rcases hg γ with ⟨i, rfl⟩
Cleared hypotheses: γ
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
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 : ℤ
⊢ ((ρ : (a : G) → V →ₗ[k] V) ((fun (x : ℤ) ↦ g ^ x) i) : (a : V) → V) x = x
have 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
Tactic: induction i with | zero => simp | succ i _ => simp_all [zpow_add_one] | pred i h => _
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
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
have 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)
Tactic: refine ⟨fun hf ↦ ⟨fun γ v ↦ ?_⟩, fun hf γ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
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)
⊢ (∀ (g : G), (σ : (a : G) → W →ₗ[k] W) g ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g⁻¹ = f) ↔ ρ.IsIntertwiningMap σ f
have refine_2 : ∀ (hf : ρ.IsIntertwiningMap σ f) (γ : G), (σ : (a : G) → W →ₗ[k] W) γ ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) γ⁻¹ = f
Tactic: refine ⟨fun hf ↦ ⟨fun γ v ↦ ?_⟩, fun hf γ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (hypothesis)
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
⊢ 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)
have hf₁ : (σ : (a : G) → W →ₗ[k] W) γ ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) γ⁻¹ = f
Tactic: specialize hf γ
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
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) ((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)
have 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)
Tactic: nth_rewrite 1 [← hf]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
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
⊢ (σ : (a : G) → W →ₗ[k] W) γ ∘ₗ f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) γ⁻¹ = f
have 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)
Tactic: ext v
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
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
⊢ 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)
have 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)
Tactic: rw [averageMap, ← asAlgebraHom_single_one, ← Module.End.mul_apply, ← map_mul (asAlgebraHom ρ),
    mul_average_left]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
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)
⊢ 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)
have 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)
Tactic: rw [averageMap, ← asAlgebraHom_single_one, ← Module.End.mul_apply, ← map_mul (asAlgebraHom ρ),
    mul_average_left]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
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)
⊢ 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)
have 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)
Tactic: rw [averageMap, ← asAlgebraHom_single_one, ← Module.End.mul_apply, ← map_mul (asAlgebraHom ρ),
    mul_average_left]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
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)
⊢ 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)
have 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)
Tactic: rw [averageMap, ← asAlgebraHom_single_one, ← Module.End.mul_apply, ← map_mul (asAlgebraHom ρ),
    mul_average_left]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (goal)
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)
⊢ 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)
have 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)
Tactic: rw [averageMap, ← asAlgebraHom_single_one, ← Module.End.mul_apply, ← map_mul (asAlgebraHom ρ),
    mul_average_left]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Invariants (hypothesis)
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
⊢ (ρ.averageMap : (a : V) → V) v = v
have hv₁ : ∀ (g : G), (((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v = v
Tactic: rw [mem_invariants] at hv
Cleared hypotheses: hv
-- 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
⊢ (((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
have 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
Tactic: dsimp
-- 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
⊢ (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
have 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
Tactic: constructor
-- 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
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
⊢ (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
have 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
Tactic: constructor
-- 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
⊢ f ∘ₗ (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: nth_rw 1 [← h]