awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A_1 : Rep k G
A B : Rep k G
f : A ⟶ B
h : H
⊢ Eq (α := (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ B)
    (Linear.rightComp k (res φ (leftRegular k H)) f ∘ₗ
        (Representation.coind' φ A : (a : H) → (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ A) h :
      (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ B)
    ((Representation.coind' φ B : (a : H) → (res φ (leftRegular k H) ⟶ B) →ₗ[k] res φ (leftRegular k H) ⟶ B) h ∘ₗ
        Linear.rightComp k (res φ (leftRegular k H)) f :
      (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ B)
have h₁ : ∀ (x : res φ (leftRegular k H) ⟶ A) (h_1 : H),
  Eq (α := (↑B : Type (max u w)))
    ((Representation.IntertwiningMap.toLinearMap
            (Hom.hom
              (((Linear.rightComp k (res φ (leftRegular k H)) f ∘ₗ
                      (Representation.coind' φ A :
                          (a : H) → (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ A)
                        h :
                    (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ B) :
                  (a : res φ (leftRegular k H) ⟶ A) → res φ (leftRegular k H) ⟶ B)
                x)) :
          (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑B : Type (max u w)))
        (single h_1 1) :
      (↑B : Type (max u w)))
    ((Representation.IntertwiningMap.toLinearMap
            (Hom.hom
              ((((Representation.coind' φ B : (a : H) → (res φ (leftRegular k H) ⟶ B) →ₗ[k] res φ (leftRegular k H) ⟶ B)
                        h ∘ₗ
                      Linear.rightComp k (res φ (leftRegular k H)) f :
                    (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ B) :
                  (a : res φ (leftRegular k H) ⟶ A) → res φ (leftRegular k H) ⟶ B)
                x)) :
          (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑B : Type (max u w)))
        (single h_1 1) :
      (↑B : Type (max u w)))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep k G
f : ↥(Representation.coindV φ A.ρ)
g : G
⊢ Eq (α := (H →₀ k) →ₗ[k] (↑A : Type (max u w)))
    (linearCombination k (↑f : H → (↑A : Type (max u w))) ∘ₗ
      (Representation.ofMulAction k H H : (a : H) → (H →₀ k) →ₗ[k] H →₀ k) ((φ : (a : G) → H) g))
    ((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g ∘ₗ
      linearCombination k (↑f : H → (↑A : Type (max u w))))
have h : ∀ (a : H),
  Eq (α := (↑A : Type (max u w)))
    (((linearCombination k (↑f : H → (↑A : Type (max u w))) ∘ₗ
            (Representation.ofMulAction k H H : (a : H) → (H →₀ k) →ₗ[k] H →₀ k) ((φ : (a : G) → H) g)) ∘ₗ
          lsingle a :
        (a : k) → (↑A : Type (max u w)))
      1)
    ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g ∘ₗ
            linearCombination k (↑f : H → (↑A : Type (max u w)))) ∘ₗ
          lsingle a :
        (a : k) → (↑A : Type (max u w)))
      1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep k G
f : res φ (leftRegular k H) ⟶ A
g : G
h : H
⊢ Eq (α := (↑A : Type (max u w)))
    ((fun (h : H) ↦
        (((Hom.hom f).toLinearMap : (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑A : Type (max u w)))
            (single h 1) :
          (↑A : Type (max u w))))
      (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h))
    ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
          (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
        (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
      ((fun (h : H) ↦
          (((Hom.hom f).toLinearMap : (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑A : Type (max u w)))
              (single h 1) :
            (↑A : Type (max u w))))
        h))
have simp : Eq (α := (↑A : Type (max u w)))
  ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) 1) :
    (↑A : Type (max u w)))
  ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
          (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
        (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
      ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single h 1)) :
    (↑A : Type (max u w)))
Tactic: simp only [res_obj_V, res_obj_ρ, Representation.IntertwiningMap.toLinearMap_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (hypothesis)
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep k G
f : res φ (leftRegular k H) ⟶ A
g : G
h : H
⊢ Eq (α := (↑A : Type (max u w)))
    ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) 1) :
      (↑A : Type (max u w)))
    ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
            (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
          (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
        ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single h 1)) :
      (↑A : Type (max u w)))
have this : Eq (α := (↑A : Type (max u w)))
  ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
          (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
        (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
      ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single h 1)) :
    (↑A : Type (max u w)))
  ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) 1) :
    (↑A : Type (max u w)))
Tactic: have := by simpa using (hom_comm_apply f g (.single h 1)).symm
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep k G
f : res φ (leftRegular k H) ⟶ A
g : G
h : H
this :
  Eq (α := (↑A : Type (max u w)))
    ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
            (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
          (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
        ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single h 1)) :
      (↑A : Type (max u w)))
    ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) 1) :
      (↑A : Type (max u w)))
⊢ Eq (α := (↑A : Type (max u w)))
    ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) 1) :
      (↑A : Type (max u w)))
    ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
            (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
          (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
        ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single h 1)) :
      (↑A : Type (max u w)))
have rw : Eq (α := (↑A : Type (max u w)))
  ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
          (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
        (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
      ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single h 1)) :
    (↑A : Type (max u w)))
  ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
          (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
        (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
      ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single h 1)) :
    (↑A : Type (max u w)))
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep k G
X Y : Rep k G
x : X ⟶ Y
⊢ CategoryTheory.Functor.map (coindFunctor k φ) x ≫ (coindIso φ Y).hom =
    (coindIso φ X).hom ≫ CategoryTheory.Functor.map (coindFunctor' k φ) x
have hf : ∀ (x_1 : (↑(Functor.obj (coindFunctor k φ) X) : Type (max u w))),
  Eq (α := (↑(Functor.obj (coindFunctor' k φ) Y) : Type (max u w)))
    (((Hom.hom (CategoryTheory.Functor.map (coindFunctor k φ) x ≫ (coindIso φ Y).hom)).toLinearMap :
          (a : (↑((coindFunctor k φ).obj X) : Type (max u w))) → (↑((coindFunctor' k φ).obj Y) : Type (max u w)))
        x_1 :
      (↑(Functor.obj (coindFunctor' k φ) Y) : Type (max u w)))
    ((Representation.IntertwiningMap.toLinearMap
            (Hom.hom ((coindIso φ X).hom ≫ CategoryTheory.Functor.map (coindFunctor' k φ) x)) :
          (a : (↑((coindFunctor k φ).obj X) : Type (max u w))) → (↑((coindFunctor' k φ).obj Y) : Type (max u w)))
        x_1 :
      (↑(Functor.obj (coindFunctor' k φ) Y) : Type (max u w)))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A_1 : Rep k G
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
⊢ Eq (α := (↑B : Type (max w u_1)) →ₗ[k] ↥(Representation.coindV φ A.ρ))
    (LinearMap.codRestrict (Representation.coindV φ A.ρ)
        (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
          (Hom.hom f).toLinearMap ∘ₗ (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
        ⋯ ∘ₗ
      (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) g)
    ((Representation.coind φ A.ρ : (a : H) → ↥(Representation.coindV φ A.ρ) →ₗ[k] ↥(Representation.coindV φ A.ρ)) g ∘ₗ
      LinearMap.codRestrict (Representation.coindV φ A.ρ)
        (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
          (Hom.hom f).toLinearMap ∘ₗ (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
        ⋯)
have dsimp : Eq (α := (↑B : Type (max w u_1)) →ₗ[k] ↥(Representation.coindV φ A.ρ))
  (LinearMap.codRestrict (Representation.coindV φ A.ρ)
      (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
        (Hom.hom f).toLinearMap ∘ₗ (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
      sorry ∘ₗ
    (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) g)
  (LinearMap.restrict (LinearMap.funLeft k (↑A : Type (max u_1 w)) fun (x : H) ↦ x * g) sorry ∘ₗ
    LinearMap.codRestrict (Representation.coindV φ A.ρ)
      (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
        (Hom.hom f).toLinearMap ∘ₗ (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
      sorry)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A_1 : Rep k G
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
⊢ Eq (α := (↑B : Type (max w u_1)) →ₗ[k] ↥(Representation.coindV φ A.ρ))
    (LinearMap.codRestrict (Representation.coindV φ A.ρ)
        (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
          (Hom.hom f).toLinearMap ∘ₗ (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
        ⋯ ∘ₗ
      (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) g)
    (LinearMap.restrict (LinearMap.funLeft k (↑A : Type (max u_1 w)) fun (x : H) ↦ x * g) ⋯ ∘ₗ
      LinearMap.codRestrict (Representation.coindV φ A.ρ)
        (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
          (Hom.hom f).toLinearMap ∘ₗ (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
        ⋯)
have h : ∀ (x : (↑B : Type (max w u_1))) (x_1 : H),
  Eq (α := (↑A : Type (max u_1 w)))
    ((↑((LinearMap.codRestrict (Representation.coindV φ A.ρ)
                  (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
                    (Hom.hom f).toLinearMap ∘ₗ
                      (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
                  sorry ∘ₗ
                (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) g :
              (a : (↑B : Type (max w u_1))) → ↥(Representation.coindV φ A.ρ))
            x) :
        H → (↑A : Type (max u_1 w)))
      x_1)
    ((↑((LinearMap.restrict (LinearMap.funLeft k (↑A : Type (max u_1 w)) fun (x : H) ↦ x * g) sorry ∘ₗ
                LinearMap.codRestrict (Representation.coindV φ A.ρ)
                  (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
                    (Hom.hom f).toLinearMap ∘ₗ
                      (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
                  sorry :
              (a : (↑B : Type (max w u_1))) → ↥(Representation.coindV φ A.ρ))
            x) :
        H → (↑A : Type (max u_1 w)))
      x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep.{?u.234193, u, v} k G
X : Rep.{max w t, u, w} k H
Y Y' : Rep.{max w t, u, v} k G
f : Functor.obj (resFunctor φ) X ⟶ Y
g : Y ⟶ Y'
⊢ Eq (α := X ⟶ Functor.obj (coindFunctor k φ) Y')
    (((resCoindHomEquiv.{t, u, v, w} φ X Y').toEquiv : (a : (resFunctor φ).obj X ⟶ Y') → X ⟶ (coindFunctor k φ).obj Y')
        (f ≫ g) :
      X ⟶ Functor.obj (coindFunctor k φ) Y')
    (((resCoindHomEquiv.{t, u, v, w} φ X Y).toEquiv : (a : (resFunctor φ).obj X ⟶ Y) → X ⟶ (coindFunctor k φ).obj Y) f ≫
        CategoryTheory.Functor.map (coindFunctor k φ) g :
      X ⟶ Functor.obj (coindFunctor k φ) Y')
have hf : ∀ (x : (↑X : Type (max t w))),
  Eq (α := (↑(Functor.obj (coindFunctor k φ) Y') : Type (max t w)))
    ((Representation.IntertwiningMap.toLinearMap
            (Hom.hom
              (((resCoindHomEquiv.{t, u, v, w} φ X Y').toEquiv :
                  (a : (resFunctor φ).obj X ⟶ Y') → X ⟶ (coindFunctor k φ).obj Y')
                (f ≫ g))) :
          (a : (↑X : Type (max t w))) → (↑((coindFunctor k φ).obj Y') : Type (max t w)))
        x :
      (↑(Functor.obj (coindFunctor k φ) Y') : Type (max t w)))
    ((Representation.IntertwiningMap.toLinearMap
            (Hom.hom
              (((resCoindHomEquiv.{t, u, v, w} φ X Y).toEquiv :
                    (a : (resFunctor φ).obj X ⟶ Y) → X ⟶ (coindFunctor k φ).obj Y)
                  f ≫
                CategoryTheory.Functor.map (coindFunctor k φ) g)) :
          (a : (↑X : Type (max t w))) → (↑((coindFunctor k φ).obj Y') : Type (max t w)))
        x :
      (↑(Functor.obj (coindFunctor k φ) Y') : Type (max t w)))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinvariants (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommRing k
inst_1 : Monoid G
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
⊢ map ρ ρ (IntertwiningMap.id ρ) = LinearMap.id
have H : ∀ (x : V),
  Eq (α := ρ.Coinvariants) ((map ρ ρ (IntertwiningMap.id ρ) ∘ₗ mk ρ : (a : V) → ρ.Coinvariants) x : ρ.Coinvariants)
    ((LinearMap.id ∘ₗ mk ρ : (a : V) → ρ.Coinvariants) x : ρ.Coinvariants)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinvariants (goal)
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ : Representation k_1 G_1 W
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
ρ : Representation k G V
S : Subgroup G
inst_12 : S.Normal
g : ↥S
⊢ Eq.{u_8 + 1} (α := Coinvariants (MonoidHom.comp ρ S.subtype) →ₗ[k] Coinvariants (MonoidHom.comp ρ S.subtype))
    ((MonoidHom.comp (ρ.toCoinvariants S) S.subtype :
          (a : ↥S) → Coinvariants (MonoidHom.comp ρ S.subtype) →ₗ[k] Coinvariants (MonoidHom.comp ρ S.subtype))
        g :
      Coinvariants (MonoidHom.comp ρ S.subtype) →ₗ[k] Coinvariants (MonoidHom.comp ρ S.subtype))
    (LinearMap.id : Coinvariants (MonoidHom.comp ρ S.subtype) →ₗ[k] Coinvariants (MonoidHom.comp ρ S.subtype))
have H : ∀ (x : V),
  Eq (α := Coinvariants (MonoidHom.comp ρ S.subtype))
    (((MonoidHom.comp (ρ.toCoinvariants S) S.subtype :
                (a : ↥S) → Coinvariants (MonoidHom.comp ρ S.subtype) →ₗ[k] Coinvariants (MonoidHom.comp ρ S.subtype))
              g ∘ₗ
            mk (MonoidHom.comp ρ S.subtype) :
          (a : V) → Coinvariants (MonoidHom.comp ρ S.subtype))
        x :
      Coinvariants (MonoidHom.comp ρ S.subtype))
    ((LinearMap.id ∘ₗ mk (MonoidHom.comp ρ S.subtype) : (a : V) → Coinvariants (MonoidHom.comp ρ S.subtype)) x :
      Coinvariants (MonoidHom.comp ρ S.subtype))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinvariants (goal)
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ : Representation k_1 G_1 W
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
ρ : Representation k G V
α : Type u_9
x : G
⊢ Eq (α := (α →₀ V) →ₗ[k] Finsupp.{u_9, u_8} α ρ.Coinvariants)
    (mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ (ρ.finsupp α : (a : G) → (α →₀ V) →ₗ[k] α →₀ V) x)
    (mapRange.linearMap (Coinvariants.mk ρ))
have h : ∀ (a : α) (x_1 : V) (a_1 : α),
  Eq.{u_8 + 1} (α := ρ.Coinvariants)
    (((((mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ (ρ.finsupp α : (a : G) → (α →₀ V) →ₗ[k] α →₀ V) x) ∘ₗ lsingle a :
                (a : V) → α →₀ ρ.Coinvariants)
              x_1 :
            Finsupp.{u_9, u_8} α ρ.Coinvariants) :
          (a : α) → ρ.Coinvariants)
        a_1 :
      ρ.Coinvariants)
    ((((mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ lsingle a : (a : V) → α →₀ ρ.Coinvariants) x_1 :
            Finsupp.{u_9, u_8} α ρ.Coinvariants) :
          (a : α) → ρ.Coinvariants)
        a_1 :
      ρ.Coinvariants)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinvariants (goal)
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ : Representation k_1 G_1 W
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
ρ : Representation k G V
α : Type u_9
⊢ ρ.coinvariantsToFinsupp α ∘ₗ ρ.finsuppToCoinvariants α = LinearMap.id
have h : ∀ (a : α) (x : V) (a_1 : α),
  Eq.{u_8 + 1} (α := ρ.Coinvariants)
    ((((((ρ.coinvariantsToFinsupp α ∘ₗ ρ.finsuppToCoinvariants α) ∘ₗ lsingle a) ∘ₗ Coinvariants.mk ρ :
                (a : V) → α →₀ ρ.Coinvariants)
              x :
            Finsupp.{u_9, u_8} α ρ.Coinvariants) :
          (a : α) → ρ.Coinvariants)
        a_1 :
      ρ.Coinvariants)
    (((((LinearMap.id ∘ₗ lsingle a) ∘ₗ Coinvariants.mk ρ : (a : V) → α →₀ ρ.Coinvariants) x :
            Finsupp.{u_9, u_8} α ρ.Coinvariants) :
          (a : α) → ρ.Coinvariants)
        a_1 :
      ρ.Coinvariants)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinvariants (goal)
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ : Representation k_1 G_1 W
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
ρ : Representation k G V
α : Type u_9
⊢ ρ.finsuppToCoinvariants α ∘ₗ ρ.coinvariantsToFinsupp α = LinearMap.id
have H : ∀ (a : α) (x : V),
  Eq (α := (ρ.finsupp α).Coinvariants)
    ((((ρ.finsuppToCoinvariants α ∘ₗ ρ.coinvariantsToFinsupp α) ∘ₗ Coinvariants.mk (ρ.finsupp α)) ∘ₗ lsingle a :
          (a : V) → (ρ.finsupp α).Coinvariants)
        x :
      (ρ.finsupp α).Coinvariants)
    (((LinearMap.id ∘ₗ Coinvariants.mk (ρ.finsupp α)) ∘ₗ lsingle a : (a : V) → (ρ.finsupp α).Coinvariants) x :
      (ρ.finsupp α).Coinvariants)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinvariants (goal)
Goal:
k_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
X : Type u_5
inst : CommRing k_1
inst_1 : Monoid G_1
inst_2 : AddCommGroup V_1
inst_3 : Module k_1 V_1
inst_4 : AddCommGroup W_1
inst_5 : Module k_1 W_1
inst_6 : AddCommGroup X
inst_7 : Module k_1 X
ρ_1 : Representation k_1 G_1 V_1
τ_1 : Representation k_1 G_1 W_1
υ : Representation k_1 G_1 X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst_8 : CommRing k
inst_9 : Group G
inst_10 : AddCommGroup V
inst_11 : Module k V
inst_12 : AddCommGroup W
inst_13 : Module k W
ρ : Representation k G V
τ : Representation k G W
x : G
⊢ Eq (α := TensorProduct k V (G →₀ k) →ₗ[k] V)
    ((TensorProduct.lift (linearCombination k fun (g : G) ↦ (ρ : (a : G) → V →ₗ[k] V) g⁻¹) ∘ₗ
        (↑(_root_.TensorProduct.comm k V (G →₀ k)) : TensorProduct k V (G →₀ k) →ₗ[k] TensorProduct k (G →₀ k) V)) ∘ₗ
      (ρ.tprod (leftRegular k G) : (a : G) → TensorProduct k V (G →₀ k) →ₗ[k] TensorProduct k V (G →₀ k)) x)
    (TensorProduct.lift (linearCombination k fun (g : G) ↦ (ρ : (a : G) → V →ₗ[k] V) g⁻¹) ∘ₗ
      (↑(_root_.TensorProduct.comm k V (G →₀ k)) : TensorProduct k V (G →₀ k) →ₗ[k] TensorProduct k (G →₀ k) V))
have a : ∀ (x_1 : V) (a : G),
  Eq.{u_8 + 1} (α := V)
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((TensorProduct.lift (linearCombination k fun (g : G) ↦ (ρ : (a : G) → V →ₗ[k] V) g⁻¹) ∘ₗ
                        (↑(_root_.TensorProduct.comm k V (G →₀ k)) :
                          TensorProduct k V (G →₀ k) →ₗ[k] TensorProduct k (G →₀ k) V)) ∘ₗ
                      (ρ.tprod (leftRegular k G) :
                          (a : G) → TensorProduct k V (G →₀ k) →ₗ[k] TensorProduct k V (G →₀ k))
                        x) :
                  V →ₗ[k] (G →₀ k) →ₗ[k] V) :
                (a : V) → (G →₀ k) →ₗ[k] V)
              x_1 ∘ₗ
            lsingle a :
          (a : k) → V)
        1 :
      V)
    ((((TensorProduct.AlgebraTensorModule.curry
                    (TensorProduct.lift (linearCombination k fun (g : G) ↦ (ρ : (a : G) → V →ₗ[k] V) g⁻¹) ∘ₗ
                      (↑(_root_.TensorProduct.comm k V (G →₀ k)) :
                        TensorProduct k V (G →₀ k) →ₗ[k] TensorProduct k (G →₀ k) V)) :
                  V →ₗ[k] (G →₀ k) →ₗ[k] V) :
                (a : V) → (G →₀ k) →ₗ[k] V)
              x_1 ∘ₗ
            lsingle a :
          (a : k) → V)
        1 :
      V)
Tactic: ext