awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Coinvariants
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
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:
simp [hom_comm_apply]

Premises used: Rep.hom_comm_apply
-- Module: Mathlib.RepresentationTheory.Coinvariants
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
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' := ⋯ })) ∘ₗ
                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))
⊢ 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))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinvariants
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
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' := ⋯ })) ∘ₗ
              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:
simp
-- Module: Mathlib.RepresentationTheory.Coinvariants
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 Z : Rep.{w, u, v} k G
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X : Type w)
⊢ Eq (α := (↑(of ((Z.toCoinvariants S).ρ.ofQuotient S)) : Type w))
    (((IntertwiningMap.toLinearMap.{u, v, w, w} (G := G ⧸ S) (ρ := ρ (of ((X.toCoinvariants S).ρ.ofQuotient S))) (σ :=
                ρ (of ((Z.toCoinvariants S).ρ.ofQuotient S)))
                (Hom.hom
                  (ofHom
                    {
                      toLinearMap :=
                        ModuleCat.Hom.hom
                          (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                            (CategoryTheory.Functor.map (resFunctor S.subtype) (f ≫ g))),
                      isIntertwining' := ⋯ })) ∘ₗ
              Coinvariants.mk (MonoidHom.comp X.ρ S.subtype) :
            (↑X : Type w) →ₗ[k] (↑(of ((Z.toCoinvariants S).ρ.ofQuotient S)) : Type w)) :
          (a : (↑X : Type w)) → (↑(of ((Z.toCoinvariants S).ρ.ofQuotient S)) : Type w))
        x :
      (↑(of ((Z.toCoinvariants S).ρ.ofQuotient S)) : Type w))
    (((IntertwiningMap.toLinearMap.{u, v, w, w} (G := G ⧸ S) (ρ := ρ (of ((X.toCoinvariants S).ρ.ofQuotient S))) (σ :=
                ρ (of ((Z.toCoinvariants S).ρ.ofQuotient S)))
                (Hom.hom
                  (CategoryStruct.comp (Y := Y.quotientToCoinvariants S)
                    (ofHom
                      {
                        toLinearMap :=
                          ModuleCat.Hom.hom
                            (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                              (CategoryTheory.Functor.map (resFunctor S.subtype) f)),
                        isIntertwining' := ⋯ })
                    (ofHom
                      {
                        toLinearMap :=
                          ModuleCat.Hom.hom
                            (CategoryTheory.Functor.map (coinvariantsFunctor k ↥S)
                              (CategoryTheory.Functor.map (resFunctor S.subtype) g)),
                        isIntertwining' := ⋯ }))) ∘ₗ
              Coinvariants.mk (MonoidHom.comp X.ρ S.subtype) :
            (↑X : Type w) →ₗ[k] (↑(of ((Z.toCoinvariants S).ρ.ofQuotient S)) : Type w)) :
          (a : (↑X : Type w)) → (↑(of ((Z.toCoinvariants S).ρ.ofQuotient S)) : Type w))
        x :
      (↑(of ((Z.toCoinvariants S).ρ.ofQuotient S)) : Type w))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
α : Type u
inst_2 : DecidableEq α
x : (↑A : Type u)
i : α
g : G
r : k
⊢ Eq (α := α →₀ (↑A : Type u))
    ((A.coinvariantsTensorFreeToFinsupp α :
          (a : (A.ρ.tprod (Representation.free k G α)).Coinvariants) → α →₀ (↑A : Type u))
        ((Coinvariants.mk (A.ρ.tprod (Representation.free k G α)) :
            (a : TensorProduct k (↑A : Type u) (α →₀ G →₀ k)) → (A.ρ.tprod (Representation.free k G α)).Coinvariants)
          (x ⊗ₜ[k] single i (single g r))) :
      α →₀ (↑A : Type u))
    (single i
        (HSMul.hSMul (β := (↑A : Type u)) r
          ((((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))
              x :
            (↑A : Type u))) :
      α →₀ (↑A : Type u))

Tactic:
simp [coinvariantsTensorFreeToFinsupp, Representation.finsuppTensorRight]

Premises used: Rep.coinvariantsTensorFreeToFinsupp, Representation.finsuppTensorRight
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
α : Type u
inst_2 : DecidableEq α
i : α
x : (↑A : Type u)
⊢ Eq (α := (A.ρ.tprod (Representation.free k G α)).Coinvariants)
    ((A.finsuppToCoinvariantsTensorFree α :
          (a : α →₀ (↑A : Type u)) → (A.ρ.tprod (Representation.free k G α)).Coinvariants)
        (single i x) :
      (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)
        (x ⊗ₜ[k] single i (single 1 1)) :
      (A.ρ.tprod (Representation.free k G α)).Coinvariants)

Tactic:
simp [finsuppToCoinvariantsTensorFree, Representation.finsuppTensorRight, Equiv.mk_symm]

Premises used: Representation.finsuppTensorRight, Rep.finsuppToCoinvariantsTensorFree, Representation.Equiv.mk_symm
-- Module: Mathlib.RepresentationTheory.Coinvariants
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 α
i : α
x : (↑A : Type u)
⊢ Eq (α := α →₀ (↑A : Type u))
    ((A.coinvariantsTensorFreeToFinsupp α ∘ₗ A.finsuppToCoinvariantsTensorFree α :
          (a : α →₀ (↑A : Type u)) → α →₀ (↑A : Type u))
        (single i x) :
      α →₀ (↑A : Type u))
    ((LinearMap.id : (a : α →₀ (↑A : Type u)) → α →₀ (↑A : Type u)) (single i x) : α →₀ (↑A : Type u))

Tactic:
simp [finsuppToCoinvariantsTensorFree_single,
        coinvariantsTensorFreeToFinsupp_mk_tmul_single]

Premises used: Rep.finsuppToCoinvariantsTensorFree_single, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single
-- Module: Mathlib.RepresentationTheory.Coinvariants
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
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)
⊢ 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)

Tactic:
simp [coinvariantsTensorFreeToFinsupp_mk_tmul_single _,
          finsuppToCoinvariantsTensorFree_single (A := A) i, TensorProduct.smul_tmul]

Premises used: TensorProduct.smul_tmul, Rep.finsuppToCoinvariantsTensorFree_single, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single
-- Module: Mathlib.RepresentationTheory.Coinvariants
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
α : Type u
inst_2 : DecidableEq α
x : (tensorObj (𝒞 := instCategory) A (free k G α)).ρ.Coinvariants
⊢ Eq (α := α →₀ (↑A : Type u))
    ((A.coinvariantsTensorFreeToFinsupp α : (a : (A ⊗ free k G α).ρ.Coinvariants) → α →₀ (↑A : Type u)) x :
      α →₀ (↑A : Type u))
    ((A.coinvariantsTensorFreeToFinsupp α : (a : (A ⊗ free k G α).ρ.Coinvariants) → α →₀ (↑A : Type u)) x :
      α →₀ (↑A : Type u))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
g : G
⊢ Eq (α := V →L[R] V)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id R) (ContinuousLinearMap.id R V) ((π₁ : (a : G) → V →L[R] V) g))
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id R) ((π₁ : (a : G) → V →L[R] V) g) (ContinuousLinearMap.id R V))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
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
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
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 }
⊢ { toContinuousLinearMap := toContinuousLinearMap, isIntertwining' := isIntertwining' : π₁ →ⁱL π₂ } = g

Tactic:
cases g
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
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
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:
congr
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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
⊢ Function.Injective (β := V →L[R] W) fun (f : π₁ →ⁱL π₂) ↦ f.toContinuousLinearMap

Tactic:
fun _ _ ↦ ext

Premises used: ContIntertwiningMap.ext, Function.Injective
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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)
h₁ :
  ∀ (x : V),
    Eq.{u_4 + 1} (α := W) ((f.toContinuousLinearMap : (a : V) → W) x : W)
      ((g.toContinuousLinearMap : (a : V) → W) x : W)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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)
x : V
⊢ Eq.{u_4 + 1} (α := W) ((f.toContinuousLinearMap : (a : V) → W) x : W) ((g.toContinuousLinearMap : (a : V) → W) x : W)

Tactic:
congr_fun h x

Premises used: congr_fun
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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)
x : V
⊢ Eq.{u_4 + 1} (α := W) ((f.toContinuousLinearMap : (a : V) → W) x : W) ((g.toContinuousLinearMap : (a : V) → W) x : W)

Tactic:
exact congr_fun h x

Premises used: congr_fun
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
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 : π₁ →ⁱL π₂
g : G
v : V
⊢ Eq (α := W) ((f : (a : V) → W) ((((π₁ : (a : G) → V →L[R] V) g : V →L[R] V) : (a : V) → V) v : V) : W)
    ((((π₂ : (a : G) → W →L[R] W) g : W →L[R] W) : (a : W) → W) ((f : (a : V) → W) v : W) : W)

Tactic:
f.toIntertwiningMap.isIntertwining _ _ g v

Premises used: ContIntertwiningMap.toIntertwiningMap, Representation.IntertwiningMap.isIntertwining