awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ρ.ofCoinvariantsTprodLeftRegular ∘ₗ
      Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ
        (LinearMap.flip (TensorProduct.mk k V (G →₀ k)) : (a : G →₀ k) → V →ₗ[k] TensorProduct k V (G →₀ k))
          (single 1 1) =
    LinearMap.id
have h : ∀ (x : V),
  Eq (α := V)
    ((ρ.ofCoinvariantsTprodLeftRegular ∘ₗ
            Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ
              (LinearMap.flip (TensorProduct.mk k V (G →₀ k)) : (a : G →₀ k) → V →ₗ[k] TensorProduct k V (G →₀ k))
                (single 1 1) :
          (a : V) → V)
        x :
      V)
    ((LinearMap.id : (a : V) → V) x : V)
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
⊢ (Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ
        (LinearMap.flip (TensorProduct.mk k V (G →₀ k)) : (a : G →₀ k) → V →ₗ[k] TensorProduct k V (G →₀ k))
          (single 1 1)) ∘ₗ
      ρ.ofCoinvariantsTprodLeftRegular =
    LinearMap.id
have H : ∀ (x : V) (a : G),
  Eq (α := (ρ.tprod (leftRegular k G)).Coinvariants)
    ((((TensorProduct.AlgebraTensorModule.curry
                  (((Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ
                        (LinearMap.flip (TensorProduct.mk k V (G →₀ k)) :
                            (a : G →₀ k) → V →ₗ[k] TensorProduct k V (G →₀ k))
                          (single 1 1)) ∘ₗ
                      ρ.ofCoinvariantsTprodLeftRegular) ∘ₗ
                    Coinvariants.mk (ρ.tprod (leftRegular k G))) :
                V →ₗ[k] (G →₀ k) →ₗ[k] (ρ.tprod (leftRegular k G)).Coinvariants) :
              (a : V) → (G →₀ k) →ₗ[k] (ρ.tprod (leftRegular k G)).Coinvariants)
            x ∘ₗ
          lsingle a :
        (a : k) → (ρ.tprod (leftRegular k G)).Coinvariants)
      1)
    ((((TensorProduct.AlgebraTensorModule.curry (LinearMap.id ∘ₗ Coinvariants.mk (ρ.tprod (leftRegular k G))) :
                V →ₗ[k] (G →₀ k) →ₗ[k] (ρ.tprod (leftRegular k G)).Coinvariants) :
              (a : V) → (G →₀ k) →ₗ[k] (ρ.tprod (leftRegular k G)).Coinvariants)
            x ∘ₗ
          lsingle a :
        (a : k) → (ρ.tprod (leftRegular k G)).Coinvariants)
      1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinvariants (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
A : Rep.{w, u, v} k G
S : Subgroup G
inst_2 : S.Normal
g : G
⊢ (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype ∘ₗ
      (A.ρ.toCoinvariantsKer S :
          (a : G) →
            ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)) →ₗ[k] ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)))
        g =
    (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g ∘ₗ (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype
have h : ∀ (x : ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))),
  Eq (α := (↑A : Type w))
    (((Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype ∘ₗ
            (A.ρ.toCoinvariantsKer S :
                (a : G) →
                  ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)) →ₗ[k]
                    ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)))
              g :
          (a : ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))) → (↑A : Type w))
        x :
      (↑A : Type w))
    (((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g ∘ₗ
            (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype :
          (a : ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))) → (↑A : Type w))
        x :
      (↑A : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinvariants (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
A : Rep.{w, u, v} k G
S : Subgroup G
inst_2 : S.Normal
⊢ Eq (α := A.toCoinvariantsKer S ⟶ A.toCoinvariants S)
    (ofHom { toLinearMap := (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype, isIntertwining' := ⋯ } ≫
      A.toCoinvariantsMkQ S)
    0
have hf : ∀ (x : (↑(A.toCoinvariantsKer S) : Type w)),
  Eq (α := (↑(A.toCoinvariants S) : Type w))
    ((IntertwiningMap.toLinearMap
            (Hom.hom
              (ofHom
                  { toLinearMap := (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype, isIntertwining' := sorry :
                    (A.ρ.toCoinvariantsKer S).IntertwiningMap A.ρ } ≫
                A.toCoinvariantsMkQ S)) :
          (a : (↑(A.toCoinvariantsKer S) : Type w)) → (↑(A.toCoinvariants S) : Type w))
        x :
      (↑(A.toCoinvariants S) : Type w))
    ((IntertwiningMap.toLinearMap (Hom.hom 0) :
          (a : (↑(A.toCoinvariantsKer S) : Type w)) → (↑(A.toCoinvariants S) : Type w))
        x :
      (↑(A.toCoinvariants S) : Type w))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinvariants (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B X Y Z : Rep.{w, u, v} k G
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ ModuleCat.ofHom (Coinvariants.map X.ρ Z.ρ (Hom.hom (x ≫ x_1))) =
    ModuleCat.ofHom (Coinvariants.map X.ρ Y.ρ (Hom.hom x)) ≫ ModuleCat.ofHom (Coinvariants.map Y.ρ Z.ρ (Hom.hom x_1))
have hf : ∀ (x_2 : (↑X : Type w)),
  Eq (α := (↑(ModuleCat.of k Z.ρ.Coinvariants) : Type w))
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (Coinvariants.map X.ρ Z.ρ (Hom.hom (x ≫ x_1)))) ∘ₗ Coinvariants.mk X.ρ :
          (a : (↑X : Type w)) → (↑(ModuleCat.of k Z.ρ.Coinvariants) : Type w))
        x_2 :
      (↑(ModuleCat.of k Z.ρ.Coinvariants) : Type w))
    ((ModuleCat.Hom.hom
              (ModuleCat.ofHom (Coinvariants.map X.ρ Y.ρ (Hom.hom x)) ≫
                ModuleCat.ofHom (Coinvariants.map Y.ρ Z.ρ (Hom.hom x_1))) ∘ₗ
            Coinvariants.mk X.ρ :
          (a : (↑X : Type w)) → (↑(ModuleCat.of k Z.ρ.Coinvariants) : Type w))
        x_2 :
      (↑(ModuleCat.of k Z.ρ.Coinvariants) : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinvariants (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B X : Rep.{w, u, v} k G
g : G
⊢ ModuleCat.Hom.hom (NatTrans.app (coinvariantsMk k G) X) ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g =
    (Representation.trivial k G (↑(Functor.obj (coinvariantsFunctor k G) X) : Type w) :
          (a : G) → (↑((coinvariantsFunctor k G).obj X) : Type w) →ₗ[k] (↑((coinvariantsFunctor k G).obj X) : Type w))
        g ∘ₗ
      ModuleCat.Hom.hom (NatTrans.app (coinvariantsMk k G) X)
have h : ∀ (x : (↑X : Type w)),
  Eq (α := (↑(Functor.obj (coinvariantsFunctor k G) X) : Type w))
    ((ModuleCat.Hom.hom (NatTrans.app (coinvariantsMk k G) X) ∘ₗ (X.ρ : (a : G) → (↑X : Type w) →ₗ[k] (↑X : Type w)) g :
          (a : (↑X : Type w)) → (↑((coinvariantsFunctor k G).obj X) : Type w))
        x :
      (↑(Functor.obj (coinvariantsFunctor k G) X) : Type w))
    (((Representation.trivial k G (↑(Functor.obj (coinvariantsFunctor k G) X) : Type w) :
                (a : G) →
                  (↑((coinvariantsFunctor k G).obj X) : Type w) →ₗ[k] (↑((coinvariantsFunctor k G).obj X) : Type w))
              g ∘ₗ
            ModuleCat.Hom.hom (NatTrans.app (coinvariantsMk k G) X) :
          (a : (↑X : Type w)) → (↑((coinvariantsFunctor k G).obj X) : Type w))
        x :
      (↑(Functor.obj (coinvariantsFunctor k G) X) : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinvariants (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X : Rep.{w, u, v} k G
Y : ModuleCat.{w, u} k
f : X ⟶ Functor.obj (trivialFunctor k G) Y
⊢ ((Adjunction.homEquiv (coinvariantsAdjunction k G) X Y).symm :
        (a : X ⟶ (trivialFunctor k G).obj Y) → (coinvariantsFunctor k G).obj X ⟶ Y)
      f =
    desc f
have hfg : ∀
  (x :
    (↑(Functor.obj
          (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
            (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
            ModuleCat.carrier))
          X) :
      Type w)),
  Eq (α := (↑Y : Type w))
    ((ModuleCat.Hom.hom
            (NatTrans.app (coinvariantsMk k G) X ≫
              ((Adjunction.homEquiv (coinvariantsAdjunction k G) X Y).symm :
                  (a : X ⟶ (trivialFunctor k G).obj Y) → (coinvariantsFunctor k G).obj X ⟶ Y)
                f) :
          (a : (↑((forget₂ (Rep k G) (ModuleCat k)).obj X) : Type w)) → (↑Y : Type w))
        x :
      (↑Y : Type w))
    ((ModuleCat.Hom.hom (NatTrans.app (coinvariantsMk k G) X ≫ desc f) :
          (a : (↑((forget₂ (Rep k G) (ModuleCat k)).obj X) : Type w)) → (↑Y : Type w))
        x :
      (↑Y : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinvariants (goal)
Goal:
k_1 : Type u
G_1 : Type v
inst : CommRing k_1
inst_1 : Monoid G_1
A B : Rep.{w, u, v} k_1 G_1
k : Type u
G : Type v
inst_2 : CommRing k
inst_3 : Group G
S : Subgroup G
inst_4 : S.Normal
X Y : Rep.{w, u, v} k G
f : X ⟶ Y
g_1 : G ⧸ S
g : G
⊢ Eq (α := (↑(X.toCoinvariants S) : Type w) →ₗ[k] (↑(Y.toCoinvariants S) : Type w))
    (ModuleCat.Hom.hom
          (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
            (CategoryTheory.Functor.map (resFunctor S.subtype) f)) ∘ₗ
        (((X.toCoinvariants S).ρ.ofQuotient S : Representation.{u, v, w} k (G ⧸ S) (↑(X.toCoinvariants S) : Type w)) :
            (a : G ⧸ S) → (↑(X.toCoinvariants S) : Type w) →ₗ[k] (↑(X.toCoinvariants S) : Type w))
          (↑g : G ⧸ S) :
      (↑(X.toCoinvariants S) : Type w) →ₗ[k] (↑(Y.toCoinvariants S) : Type w))
    ((((Y.toCoinvariants S).ρ.ofQuotient S : Representation.{u, v, w} k (G ⧸ S) (↑(Y.toCoinvariants S) : Type w)) :
            (a : G ⧸ S) → (↑(Y.toCoinvariants S) : Type w) →ₗ[k] (↑(Y.toCoinvariants S) : Type w))
          (↑g : G ⧸ S) ∘ₗ
        ModuleCat.Hom.hom
          (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
            (CategoryTheory.Functor.map (resFunctor S.subtype) f)) :
      (↑(X.toCoinvariants S) : Type w) →ₗ[k] (↑(Y.toCoinvariants S) : Type w))
have H : ∀ (x : (↑X : Type w)),
  Eq (α := (↑(Y.toCoinvariants S) : Type w))
    ((((ModuleCat.Hom.hom
                  (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                    (CategoryTheory.Functor.map (resFunctor S.subtype) f)) ∘ₗ
                (((X.toCoinvariants S).ρ.ofQuotient S :
                      Representation.{u, v, w} k (G ⧸ S) (↑(X.toCoinvariants S) : Type w)) :
                    (a : G ⧸ S) → (↑(X.toCoinvariants S) : Type w) →ₗ[k] (↑(X.toCoinvariants S) : Type w))
                  (↑g : G ⧸ S)) ∘ₗ
              Coinvariants.mk (MonoidHom.comp X.ρ S.subtype) :
            (↑X : Type w) →ₗ[k] (↑(Y.toCoinvariants S) : Type w)) :
          (a : (↑X : Type w)) → (↑(Y.toCoinvariants S) : Type w))
        x :
      (↑(Y.toCoinvariants S) : Type w))
    ((((((Y.toCoinvariants S).ρ.ofQuotient S : Representation.{u, v, w} k (G ⧸ S) (↑(Y.toCoinvariants S) : Type w)) :
                  (a : G ⧸ S) → (↑(Y.toCoinvariants S) : Type w) →ₗ[k] (↑(Y.toCoinvariants S) : Type w))
                (↑g : G ⧸ S) ∘ₗ
              ModuleCat.Hom.hom
                (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                  (CategoryTheory.Functor.map (resFunctor S.subtype) f))) ∘ₗ
            Coinvariants.mk (MonoidHom.comp X.ρ S.subtype) :
          (a : (↑X : Type w)) → (↑(Y.toCoinvariants S) : Type w))
        x :
      (↑(Y.toCoinvariants S) : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinvariants (goal)
Goal:
k_1 : Type u
G_1 : Type v
inst : CommRing k_1
inst_1 : Monoid G_1
A B : Rep.{w, u, v} k_1 G_1
k : Type u
G : Type v
inst_2 : CommRing k
inst_3 : Group G
S : Subgroup G
inst_4 : S.Normal
X : Rep.{w, u, v} k G
⊢ Eq (α := Quiver.Hom (V := Rep.{w, u, v} k (G ⧸ S)) (X.quotientToCoinvariants S) (X.quotientToCoinvariants S))
    (ofHom
        {
          toLinearMap :=
            ModuleCat.Hom.hom
              (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                (CategoryTheory.Functor.map (resFunctor S.subtype) (𝟙 X))),
          isIntertwining' := ⋯ } :
      Quiver.Hom (V := Rep.{w, u, v} k (G ⧸ S)) (of ((X.toCoinvariants S).ρ.ofQuotient S))
        (of ((X.toCoinvariants S).ρ.ofQuotient S)))
    (𝟙 (X.quotientToCoinvariants S) :
      Quiver.Hom (V := Rep.{w, u, v} k (G ⧸ S)) (X.quotientToCoinvariants S) (X.quotientToCoinvariants S))
have hf : ∀ (x : (↑X : Type w)),
  Eq (α := (↑(of ((X.toCoinvariants S).ρ.ofQuotient S)) : Type w))
    (((IntertwiningMap.toLinearMap.{u, v, w, w} (G := G ⧸ S) (ρ := ρ (of ((X.toCoinvariants S).ρ.ofQuotient S))) (σ :=
                ρ (of ((X.toCoinvariants S).ρ.ofQuotient S)))
                (Hom.hom
                  (ofHom
                    {
                      toLinearMap :=
                        ModuleCat.Hom.hom
                          (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                            (CategoryTheory.Functor.map (resFunctor S.subtype) (𝟙 X))),
                      isIntertwining' := sorry })) ∘ₗ
              Coinvariants.mk (MonoidHom.comp X.ρ S.subtype) :
            (↑X : Type w) →ₗ[k] (↑(of ((X.toCoinvariants S).ρ.ofQuotient S)) : Type w)) :
          (a : (↑X : Type w)) → (↑(of ((X.toCoinvariants S).ρ.ofQuotient S)) : Type w))
        x :
      (↑(of ((X.toCoinvariants S).ρ.ofQuotient S)) : Type w))
    ((IntertwiningMap.toLinearMap (Hom.hom (𝟙 (X.quotientToCoinvariants S))) ∘ₗ
            Coinvariants.mk (MonoidHom.comp X.ρ S.subtype) :
          (a : (↑X : Type w)) → (↑(of ((X.toCoinvariants S).ρ.ofQuotient S)) : Type w))
        x :
      (↑(of ((X.toCoinvariants S).ρ.ofQuotient S)) : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinvariants (goal)
Goal:
k_1 : Type u
G_1 : Type v
inst : CommRing k_1
inst_1 : Monoid G_1
A_1 B : Rep.{w, u, v} k_1 G_1
k_2 : Type u
G_2 : Type v
inst_2 : CommRing k_2
inst_3 : Group G_2
k G : Type u
inst_4 : CommRing k
inst_5 : Group G
A : Rep k G
α : Type u
inst_6 : DecidableEq α
a : (↑A : Type u)
i : α
g : G
r : k
⊢ Eq (α := (tensorObj (𝒞 := instCategory) A (free k G α)).ρ.Coinvariants)
    (((LinearMap.compr₂ₛₗ (TensorProduct.mk k (↑A : Type u) (↑(free k G α) : Type u))
                  ((A.finsuppToCoinvariantsTensorFree α ∘ₗ A.coinvariantsTensorFreeToFinsupp α) ∘ₗ
                    Coinvariants.mk (tensorObj (𝒞 := instCategory) A (free k G α)).ρ) :
                (a : (↑A : Type u)) → (↑(free k G α) : Type u) →ₗ[k] (A ⊗ free k G α).ρ.Coinvariants)
              a ∘ₗ
            lsingle i :
          (a : G →₀ k) → (A ⊗ free k G α).ρ.Coinvariants)
        (single g r) :
      (tensorObj (𝒞 := instCategory) A (free k G α)).ρ.Coinvariants)
    (((LinearMap.compr₂ₛₗ (TensorProduct.mk k (↑A : Type u) (↑(free k G α) : Type u))
                  (LinearMap.id ∘ₗ Coinvariants.mk (tensorObj (𝒞 := instCategory) A (free k G α)).ρ) :
                (a : (↑A : Type u)) → (↑(free k G α) : Type u) →ₗ[k] (A ⊗ free k G α).ρ.Coinvariants)
              a ∘ₗ
            lsingle i :
          (a : G →₀ k) → (A ⊗ free k G α).ρ.Coinvariants)
        (single g r) :
      (tensorObj (𝒞 := instCategory) A (free k G α)).ρ.Coinvariants)
have simp : Eq (α := (A.ρ.tprod (Representation.free k G α)).Coinvariants)
  ((Coinvariants.mk (A.ρ.tprod (Representation.free k G α)) :
        (a : TensorProduct k (↑A : Type u) (α →₀ G →₀ k)) → (A.ρ.tprod (Representation.free k G α)).Coinvariants)
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          a ⊗ₜ[k]
        single i (single 1 r)) :
    (A.ρ.tprod (Representation.free k G α)).Coinvariants)
  ((Coinvariants.mk (A.ρ.tprod (Representation.free k G α)) :
        (a : TensorProduct k (↑A : Type u) (α →₀ G →₀ k)) → (A.ρ.tprod (Representation.free k G α)).Coinvariants)
      (a ⊗ₜ[k] single i (single g r)) :
    (A.ρ.tprod (Representation.free k G α)).Coinvariants)
Tactic: simp [coinvariantsTensorFreeToFinsupp_mk_tmul_single _,
          finsuppToCoinvariantsTensorFree_single (A := A) i, TensorProduct.smul_tmul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
f g : π₁ →ⁱL π₂
h : f.toContinuousLinearMap = g.toContinuousLinearMap
⊢ f = g
have mk : ∀ (toContinuousLinearMap : V →L[R] W)
  (isIntertwining' :
    ∀ (g : G),
      toContinuousLinearMap.comp (σ₁₂ := RingHom.id R) ((π₁ : (a : G) → V →L[R] V) g) =
        ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₂ : (a : G) → W →L[R] W) g) toContinuousLinearMap)
  (h :
    { toContinuousLinearMap := toContinuousLinearMap, isIntertwining' := isIntertwining' :
          π₁ →ⁱL π₂ }.toContinuousLinearMap =
      g.toContinuousLinearMap),
  { toContinuousLinearMap := toContinuousLinearMap, isIntertwining' := isIntertwining' : π₁ →ⁱL π₂ } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
g : π₁ →ⁱL π₂
toContinuousLinearMap : V →L[R] W
isIntertwining' :
  ∀ (g : G),
    toContinuousLinearMap.comp (σ₁₂ := RingHom.id R) ((π₁ : (a : G) → V →L[R] V) g) =
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₂ : (a : G) → W →L[R] W) g) toContinuousLinearMap
h :
  { toContinuousLinearMap := toContinuousLinearMap, isIntertwining' := isIntertwining' :
        π₁ →ⁱL π₂ }.toContinuousLinearMap =
    g.toContinuousLinearMap
⊢ { toContinuousLinearMap := toContinuousLinearMap, isIntertwining' := isIntertwining' : π₁ →ⁱL π₂ } = g
have mk : ∀ (toContinuousLinearMap_1 : V →L[R] W)
  (isIntertwining'_1 :
    ∀ (g : G),
      toContinuousLinearMap_1.comp (σ₁₂ := RingHom.id R) ((π₁ : (a : G) → V →L[R] V) g) =
        ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₂ : (a : G) → W →L[R] W) g) toContinuousLinearMap_1)
  (h :
    { toContinuousLinearMap := toContinuousLinearMap, isIntertwining' := isIntertwining' :
          π₁ →ⁱL π₂ }.toContinuousLinearMap =
      { toContinuousLinearMap := toContinuousLinearMap_1, isIntertwining' := isIntertwining'_1 :
          π₁ →ⁱL π₂ }.toContinuousLinearMap),
  { toContinuousLinearMap := toContinuousLinearMap, isIntertwining' := isIntertwining' : π₁ →ⁱL π₂ } =
    { toContinuousLinearMap := toContinuousLinearMap_1, isIntertwining' := isIntertwining'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
f g : π₁ →ⁱL π₂
h :
  Eq (α := V → W) ((fun (f : π₁ →ⁱL π₂) ↦ (↑f.toContinuousLinearMap : V →ₗ[R] W).toFun) f)
    ((fun (f : π₁ →ⁱL π₂) ↦ (↑f.toContinuousLinearMap : V →ₗ[R] W).toFun) g)
⊢ f = g
have h₁ : ∀ (x : V),
  Eq.{u_4 + 1} (α := W) ((f.toContinuousLinearMap : (a : V) → W) x : W) ((g.toContinuousLinearMap : (a : V) → W) x : W)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
inst_10 : AddCommGroup U
inst_11 : Module R U
inst_12 : TopologicalSpace U
inst_13 : IsTopologicalAddGroup U
π₁_1 : ContRepresentation R G V
π₂_1 : ContRepresentation R G W
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
h : G
⊢ (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap).comp (σ₁₂ := RingHom.id R) ((π₁ : (a : G) → V →L[R] V) h) =
    ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₃ : (a : G) → U →L[R] U) h)
      (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap)
have rw : f.toContinuousLinearMap ∘SL g.comp (σ₁₂ := RingHom.id R) ((π₁ : (a : G) → V →L[R] V) h) =
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₃ : (a : G) → U →L[R] U) h)
    (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap)
Tactic: rw [comp_assoc, g.2, ← comp_assoc, f.2, comp_assoc]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Continuous.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
inst_10 : AddCommGroup U
inst_11 : Module R U
inst_12 : TopologicalSpace U
inst_13 : IsTopologicalAddGroup U
π₁_1 : ContRepresentation R G V
π₂_1 : ContRepresentation R G W
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
h : G
rw :
  f.toContinuousLinearMap ∘SL g.comp (σ₁₂ := RingHom.id R) ((π₁ : (a : G) → V →L[R] V) h) =
    ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₃ : (a : G) → U →L[R] U) h)
      (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap)
⊢ (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap).comp (σ₁₂ := RingHom.id R) ((π₁ : (a : G) → V →L[R] V) h) =
    ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₃ : (a : G) → U →L[R] U) h)
      (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap)
have rw₁ : f.toContinuousLinearMap ∘SL
    ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₂ : (a : G) → W →L[R] W) h) g.toContinuousLinearMap =
  ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₃ : (a : G) → U →L[R] U) h)
    (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap)
Tactic: rw [comp_assoc, g.2, ← comp_assoc, f.2, comp_assoc]