awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
ι : Type u'
f : ι → (A ⟶ B)
s : Finset ι
⊢ Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ s, f i)) (∑ i ∈ s, Hom.hom (f i))
have empty : Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, Hom.hom (f i))
Tactic: classical induction s using Finset.induction with
  | empty => simp
  | insert a s ha h => simp [Finset.sum_insert ha, add_hom, h]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
ι : Type u'
f : ι → (A ⟶ B)
s : Finset ι
empty : Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, Hom.hom (f i))
⊢ Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ s, f i)) (∑ i ∈ s, Hom.hom (f i))
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (h : Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ s, f i)) (∑ i ∈ s, Hom.hom (f i))),
  Eq.{w + 1} (α := A.ρ.IntertwiningMap B.ρ) (Hom.hom (∑ i ∈ insert a s, f i)) (∑ i ∈ insert a s, Hom.hom (f i))
Tactic: classical induction s using Finset.induction with
  | empty => simp
  | insert a s ha h => simp [Finset.sum_insert ha, add_hom, h]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
ι : Type u'
M N : Type v'
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module k M
inst_5 : Module k N
σ : Representation k G M
ρ : Representation k G N
f : ι → σ.IntertwiningMap ρ
s : Finset ι
⊢ Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ s, f i)) (∑ i ∈ s, ofHom (f i))
have empty : Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, ofHom (f i))
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert a s ha h => simp [Finset.sum_insert ha, ofHom_add, h]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
ι : Type u'
M N : Type v'
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module k M
inst_5 : Module k N
σ : Representation k G M
ρ : Representation k G N
f : ι → σ.IntertwiningMap ρ
s : Finset ι
empty : Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, ofHom (f i))
⊢ Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ s, f i)) (∑ i ∈ s, ofHom (f i))
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (h : Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ s, f i)) (∑ i ∈ s, ofHom (f i))),
  Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ insert a s, f i)) (∑ i ∈ insert a s, ofHom (f i))
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert a s ha h => simp [Finset.sum_insert ha, ofHom_add, h]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
ι : Type u'
M N : Type v'
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module k M
inst_5 : Module k N
σ : Representation k G M
ρ : Representation k G N
f : ι → σ.IntertwiningMap ρ
s : Finset ι
⊢ Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ s, f i)) (∑ i ∈ s, ofHom (f i))
have empty : Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, ofHom (f i))
Tactic: classical induction s using Finset.induction with
  | empty => simp
  | insert a s ha h => simp [Finset.sum_insert ha, ofHom_add, h]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
ι : Type u'
M N : Type v'
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module k M
inst_5 : Module k N
σ : Representation k G M
ρ : Representation k G N
f : ι → σ.IntertwiningMap ρ
s : Finset ι
empty : Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ ∅, f i)) (∑ i ∈ ∅, ofHom (f i))
⊢ Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ s, f i)) (∑ i ∈ s, ofHom (f i))
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (h : Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ s, f i)) (∑ i ∈ s, ofHom (f i))),
  Eq.{v' + 1} (α := of σ ⟶ of ρ) (ofHom (∑ i ∈ insert a s, f i)) (∑ i ∈ insert a s, ofHom (f i))
Tactic: classical induction s using Finset.induction with
  | empty => simp
  | insert a s ha h => simp [Finset.sum_insert ha, ofHom_add, h]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A : Rep.{w, u, v} k G
g1 g2 : G
⊢ Eq.{w + 1} (α := (↑A : Type w) →ₗ[k] (↑A : Type w))
    ((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) (g1 * g2) : (↑A : Type w) →ₗ[k] (↑A : Type w))
    ((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g1 ∘ₗ (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g2 :
      (↑A : Type w) →ₗ[k] (↑A : Type w))
have h : ∀ (x : (↑A : Type w)),
  Eq (α := (↑A : Type w))
    ((((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) (g1 * g2) : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        x :
      (↑A : Type w))
    (((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g1 ∘ₗ (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g2 :
          (a : (↑A : Type w)) → (↑A : Type w))
        x :
      (↑A : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
inst : Semiring k
G : Type v
inst_1 : CommMonoid G
A B : Rep.{u_1, u, v} k G
f : A ⟶ B
g : G
⊢ A.applyAsHom g ≫ f = f ≫ B.applyAsHom g
have hf : ∀ (x : (↑A : Type u_1)),
  Eq (α := (↑B : Type u_1))
    (((Hom.hom (A.applyAsHom g ≫ f)).toLinearMap : (a : (↑A : Type u_1)) → (↑B : Type u_1)) x : (↑B : Type u_1))
    (((Hom.hom (f ≫ B.applyAsHom g)).toLinearMap : (a : (↑A : Type u_1)) → (↑B : Type u_1)) x : (↑B : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A : Rep k G
x : (↑A : Type (max u v))
g : G
⊢ Eq (α := (G →₀ k) →ₗ[k] (↑A : Type (max u v)))
    (((Finsupp.lift (↑A : Type (max u v)) k G : (a : G → (↑A : Type (max u v))) → (G →₀ k) →ₗ[k] (↑A : Type (max u v)))
        fun (g : G) ↦
        (((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g :
              (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) :
            (a : (↑A : Type (max u v))) → (↑A : Type (max u v)))
          x) ∘ₗ
      (Representation.ofMulAction k G G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g)
    ((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g ∘ₗ
      (Finsupp.lift (↑A : Type (max u v)) k G : (a : G → (↑A : Type (max u v))) → (G →₀ k) →ₗ[k] (↑A : Type (max u v)))
        fun (g : G) ↦
        (((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g :
              (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) :
            (a : (↑A : Type (max u v))) → (↑A : Type (max u v)))
          x)
have h : ∀ (a : G),
  Eq (α := (↑A : Type (max u v)))
    (((((Finsupp.lift (↑A : Type (max u v)) k G :
                (a : G → (↑A : Type (max u v))) → (G →₀ k) →ₗ[k] (↑A : Type (max u v)))
              fun (g : G) ↦
              (((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g :
                    (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) :
                  (a : (↑A : Type (max u v))) → (↑A : Type (max u v)))
                x) ∘ₗ
            (Representation.ofMulAction k G G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → (↑A : Type (max u v)))
      1)
    ((((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g ∘ₗ
            (Finsupp.lift (↑A : Type (max u v)) k G :
                (a : G → (↑A : Type (max u v))) → (G →₀ k) →ₗ[k] (↑A : Type (max u v)))
              fun (g : G) ↦
              (((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g :
                    (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) :
                  (a : (↑A : Type (max u v))) → (↑A : Type (max u v)))
                x) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → (↑A : Type (max u v)))
      1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommSemiring k
inst_1 : Monoid G
M N O : Rep.{u_1, u, v} k G
r : k
f : M ⟶ N
g : N ⟶ O
⊢ (r • f) ≫ g = r • f ≫ g
have hf : Hom.hom ((r • f) ≫ g) = Hom.hom (r • f ≫ g)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommSemiring k
inst_1 : Monoid G
M N O : Rep.{u_1, u, v} k G
f : M ⟶ N
r : k
g : N ⟶ O
⊢ f ≫ (r • g) = r • f ≫ g
have hf : ∀ (x : (↑M : Type u_1)),
  Eq (α := (↑O : Type u_1))
    (((Hom.hom (f ≫ (r • g))).toLinearMap : (a : (↑M : Type u_1)) → (↑O : Type u_1)) x : (↑O : Type u_1))
    (((Hom.hom (r • f ≫ g)).toLinearMap : (a : (↑M : Type u_1)) → (↑O : Type u_1)) x : (↑O : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
x : X ⟶ Y
⊢ Eq (α :=
    of (X := TensorProduct k (↑(trivial k G k) : Type u) (↑X : Type u)) (Representation.tprod (ρ (trivial k G k)) X.ρ) ⟶
      Y)
    (ofHom (lTensor (ρ (trivial k G k)) (Hom.hom x)) ≫ Iso.hom (mkIso (lid k Y.ρ))) (Iso.hom (mkIso (lid k X.ρ)) ≫ x)
have hf : ∀ (x_1 : (↑X : Type u)),
  Eq (α := (↑Y : Type u))
    ((((TensorProduct.AlgebraTensorModule.curry
                  (toLinearMap
                    (Hom.hom (ofHom (lTensor (ρ (trivial k G k)) (Hom.hom x)) ≫ Iso.hom (mkIso (lid k Y.ρ))))) :
                (↑(trivial k G k) : Type u) →ₗ[k] (↑X : Type u) →ₗ[k] (↑Y : Type u)) :
              (a : k) → (↑X : Type u) →ₗ[k] (↑Y : Type u))
            1 :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x_1 :
      (↑Y : Type u))
    ((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (Hom.hom (Iso.hom (mkIso (lid k X.ρ)) ≫ x))) :
                (↑(trivial k G k) : Type u) →ₗ[k] (↑X : Type u) →ₗ[k] (↑Y : Type u)) :
              (a : k) → (↑X : Type u) →ₗ[k] (↑Y : Type u))
            1 :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x_1 :
      (↑Y : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
x : X ⟶ Y
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 x_3 : Rep k G
⊢ ofHom (rTensor x_3.ρ (Hom.hom (mkIso (assoc x.ρ x_1.ρ x_2.ρ)).hom)) ≫
      (mkIso (assoc x.ρ (of (x_1.ρ.tprod x_2.ρ)).ρ x_3.ρ)).hom ≫
        ofHom (lTensor x.ρ (Hom.hom (mkIso (assoc x_1.ρ x_2.ρ x_3.ρ)).hom)) =
    (mkIso (assoc (of (x.ρ.tprod x_1.ρ)).ρ x_2.ρ x_3.ρ)).hom ≫ (mkIso (assoc x.ρ x_1.ρ (of (x_2.ρ.tprod x_3.ρ)).ρ)).hom
have hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Rep k G
⊢ Hom.hom (Iso.hom (α_ X Y Z)) =
    (↑(assoc X.ρ Y.ρ Z.ρ) : ((X.ρ.tprod Y.ρ).tprod Z.ρ).IntertwiningMap (X.ρ.tprod (Y.ρ.tprod Z.ρ)))
have h : toLinearMap (Hom.hom (Iso.hom (α_ X Y Z))) =
  (↑(assoc X.ρ Y.ρ Z.ρ) : ((X.ρ.tprod Y.ρ).tprod Z.ρ).IntertwiningMap (X.ρ.tprod (Y.ρ.tprod Z.ρ))).toLinearMap
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
⊢ Eq.{u + 1} (α := tensorObj (𝒞 := instCategory) x x_1 ⟶ tensorObj (𝒞 := instCategory) x x_2) (x ◁ 0) 0
have hf : Eq (α := (tensorObj (𝒞 := instCategory) x x_1).ρ.IntertwiningMap (tensorObj (𝒞 := instCategory) x x_2).ρ)
  (Hom.hom (x ◁ 0)) (Hom.hom 0)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
⊢ Eq.{u + 1} (α := tensorObj (𝒞 := instCategory) x_1 x ⟶ tensorObj (𝒞 := instCategory) x_2 x) (0 ▷ x) 0
have hf : Eq (α := (tensorObj (𝒞 := instCategory) x_1 x).ρ.IntertwiningMap (tensorObj (𝒞 := instCategory) x_2 x).ρ)
  (Hom.hom (0 ▷ x)) (Hom.hom 0)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Rep k G
x x_1 : Y ⟶ Z
⊢ X ◁ (x + x_1) =
    HAdd.hAdd (α := tensorObj (𝒞 := instCategory) X Y ⟶ tensorObj (𝒞 := instCategory) X Z) (X ◁ x) (X ◁ x_1)
have hf : Hom.hom (X ◁ (x + x_1)) =
  Hom.hom (HAdd.hAdd (α := tensorObj (𝒞 := instCategory) X Y ⟶ tensorObj (𝒞 := instCategory) X Z) (X ◁ x) (X ◁ x_1))
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Rep k G
x x_1 : Y ⟶ Z
⊢ (x + x_1) ▷ X =
    HAdd.hAdd (α := tensorObj (𝒞 := instCategory) Y X ⟶ tensorObj (𝒞 := instCategory) Z X) (x ▷ X) (x_1 ▷ X)
have hf : Hom.hom ((x + x_1) ▷ X) =
  Hom.hom (HAdd.hAdd (α := tensorObj (𝒞 := instCategory) Y X ⟶ tensorObj (𝒞 := instCategory) Z X) (x ▷ X) (x_1 ▷ X))
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
x_3 : k
x_4 : x_1 ⟶ x_2
⊢ x ◁ (x_3 • x_4) =
    HSMul.hSMul (β := tensorObj (𝒞 := instCategory) x x_1 ⟶ tensorObj (𝒞 := instCategory) x x_2) x_3 (x ◁ x_4)
have hf : Hom.hom (x ◁ (x_3 • x_4)) =
  Hom.hom (HSMul.hSMul (β := tensorObj (𝒞 := instCategory) x x_1 ⟶ tensorObj (𝒞 := instCategory) x x_2) x_3 (x ◁ x_4))
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x : k
x_1 x_2 : Rep k G
x_3 : x_1 ⟶ x_2
x_4 : Rep k G
⊢ (x • x_3) ▷ x_4 =
    HSMul.hSMul (β := tensorObj (𝒞 := instCategory) x_1 x_4 ⟶ tensorObj (𝒞 := instCategory) x_2 x_4) x (x_3 ▷ x_4)
have hf : Hom.hom ((x • x_3) ▷ x_4) =
  Hom.hom
    (HSMul.hSMul (β := tensorObj (𝒞 := instCategory) x_1 x_4 ⟶ tensorObj (𝒞 := instCategory) x_2 x_4) x (x_3 ▷ x_4))
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
x_3 : x_1 ⟶ x_2
⊢ x ◁ x_3 ≫ (mkIso (Representation.TensorProduct.comm x.ρ x_2.ρ)).hom =
    (mkIso (Representation.TensorProduct.comm x.ρ x_1.ρ)).hom ≫ x_3 ▷ x
have hf : Hom.hom (x ◁ x_3 ≫ (mkIso (Representation.TensorProduct.comm x.ρ x_2.ρ)).hom) =
  Hom.hom ((mkIso (Representation.TensorProduct.comm x.ρ x_1.ρ)).hom ≫ x_3 ▷ x)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
x : X ⟶ Y
x_1 : Rep k G
⊢ x ▷ x_1 ≫ (mkIso (Representation.TensorProduct.comm Y.ρ x_1.ρ)).hom =
    (mkIso (Representation.TensorProduct.comm X.ρ x_1.ρ)).hom ≫ x_1 ◁ x
have hf : Hom.hom (x ▷ x_1 ≫ (mkIso (Representation.TensorProduct.comm Y.ρ x_1.ρ)).hom) =
  Hom.hom ((mkIso (Representation.TensorProduct.comm X.ρ x_1.ρ)).hom ≫ x_1 ◁ x)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
x x_1 x_2 : Rep k G
⊢ Iso.hom (α_ x x_1 x_2) ≫
      (mkIso (Representation.TensorProduct.comm x.ρ (tensorObj (𝒞 := instCategory) x_1 x_2).ρ)).hom ≫
        Iso.hom (α_ x_1 x_2 x) =
    (mkIso (Representation.TensorProduct.comm x.ρ x_1.ρ)).hom ▷ x_2 ≫
      Iso.hom (α_ x_1 x x_2) ≫ x_1 ◁ (mkIso (Representation.TensorProduct.comm x.ρ x_2.ρ)).hom
have hf : (Hom.hom
      (Iso.hom (α_ x x_1 x_2) ≫
        (mkIso (Representation.TensorProduct.comm x.ρ (tensorObj (𝒞 := instCategory) x_1 x_2).ρ)).hom ≫
          Iso.hom (α_ x_1 x_2 x))).toLinearMap =
  (Hom.hom
      ((mkIso (Representation.TensorProduct.comm x.ρ x_1.ρ)).hom ▷ x_2 ≫
        Iso.hom (α_ x_1 x x_2) ≫ x_1 ◁ (mkIso (Representation.TensorProduct.comm x.ρ x_2.ρ)).hom)).toLinearMap
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Rep k G
⊢ Iso.inv (α_ X Y Z) ≫
      (mkIso (Representation.TensorProduct.comm (tensorObj (𝒞 := instCategory) X Y).ρ Z.ρ)).hom ≫ Iso.inv (α_ Z X Y) =
    X ◁ (mkIso (Representation.TensorProduct.comm Y.ρ Z.ρ)).hom ≫
      Iso.inv (α_ X Z Y) ≫ (mkIso (Representation.TensorProduct.comm X.ρ Z.ρ)).hom ▷ Y
have hf : (Hom.hom
      (Iso.inv (α_ X Y Z) ≫
        (mkIso (Representation.TensorProduct.comm (tensorObj (𝒞 := instCategory) X Y).ρ Z.ρ)).hom ≫
          Iso.inv (α_ Z X Y))).toLinearMap =
  (Hom.hom
      (X ◁ (mkIso (Representation.TensorProduct.comm Y.ρ Z.ρ)).hom ≫
        Iso.inv (α_ X Z Y) ≫ (mkIso (Representation.TensorProduct.comm X.ρ Z.ρ)).hom ▷ Y)).toLinearMap
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep k G
⊢ Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X) = 𝟙 (tensorObj (𝒞 := instCategory) X Y)
have hf : Hom.hom (Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X)) = Hom.hom (𝟙 (tensorObj (𝒞 := instCategory) X Y))
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A B C : Rep.{w, u, v} k G
X Y : Rep.{u_1, u, v} k G
f : X ⟶ Y
g : G
⊢ Eq (α :=
    LinearMap.{u, u, w, u_1} (RingHom.id k) (↑A : Type w) (↑X : Type u_1) →ₗ[k]
      LinearMap.{u, u, w, u_1} (RingHom.id k) (↑A : Type w) (↑Y : Type u_1))
    ((LinearMap.llcomp k (↑A : Type w) (↑X : Type u_1) (↑Y : Type u_1) :
          (a : (↑X : Type u_1) →ₗ[k] (↑Y : Type u_1)) →
            ((↑A : Type w) →ₗ[k] (↑X : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Y : Type u_1))
        (Hom.hom f).toLinearMap ∘ₗ
      (A.ρ.linHom X.ρ : (a : G) → ((↑A : Type w) →ₗ[k] (↑X : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑X : Type u_1)) g)
    ((A.ρ.linHom Y.ρ : (a : G) → ((↑A : Type w) →ₗ[k] (↑Y : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Y : Type u_1)) g ∘ₗ
      (LinearMap.llcomp k (↑A : Type w) (↑X : Type u_1) (↑Y : Type u_1) :
          (a : (↑X : Type u_1) →ₗ[k] (↑Y : Type u_1)) →
            ((↑A : Type w) →ₗ[k] (↑X : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Y : Type u_1))
        (Hom.hom f).toLinearMap)
have h : ∀ (x : LinearMap.{u, u, w, u_1} (RingHom.id k) (↑A : Type w) (↑X : Type u_1)) (x_1 : (↑A : Type w)),
  Eq.{u_1 + 1} (α := (↑Y : Type u_1))
    (((((LinearMap.llcomp k (↑A : Type w) (↑X : Type u_1) (↑Y : Type u_1) :
                      (a : (↑X : Type u_1) →ₗ[k] (↑Y : Type u_1)) →
                        ((↑A : Type w) →ₗ[k] (↑X : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Y : Type u_1))
                    (Hom.hom f).toLinearMap ∘ₗ
                  (A.ρ.linHom X.ρ :
                      (a : G) → ((↑A : Type w) →ₗ[k] (↑X : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑X : Type u_1))
                    g :
                (a : (↑A : Type w) →ₗ[k] (↑X : Type u_1)) → (↑A : Type w) →ₗ[k] (↑Y : Type u_1))
              x :
            LinearMap.{u, u, w, u_1} (RingHom.id k) (↑A : Type w) (↑Y : Type u_1)) :
          (a : (↑A : Type w)) → (↑Y : Type u_1))
        x_1 :
      (↑Y : Type u_1))
    (((((A.ρ.linHom Y.ρ : (a : G) → ((↑A : Type w) →ₗ[k] (↑Y : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Y : Type u_1))
                    g ∘ₗ
                  (LinearMap.llcomp k (↑A : Type w) (↑X : Type u_1) (↑Y : Type u_1) :
                      (a : (↑X : Type u_1) →ₗ[k] (↑Y : Type u_1)) →
                        ((↑A : Type w) →ₗ[k] (↑X : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑Y : Type u_1))
                    (Hom.hom f).toLinearMap :
                (a : (↑A : Type w) →ₗ[k] (↑X : Type u_1)) → (↑A : Type w) →ₗ[k] (↑Y : Type u_1))
              x :
            LinearMap.{u, u, w, u_1} (RingHom.id k) (↑A : Type w) (↑Y : Type u_1)) :
          (a : (↑A : Type w)) → (↑Y : Type u_1))
        x_1 :
      (↑Y : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A B C : Rep.{w, u, v} k G
x : Rep.{u_1, u, v} k G
⊢ ofHom
      {
        toLinearMap :=
          (LinearMap.llcomp k (↑A : Type w) (↑x : Type u_1) (↑x : Type u_1) :
              (a : (↑x : Type u_1) →ₗ[k] (↑x : Type u_1)) →
                ((↑A : Type w) →ₗ[k] (↑x : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑x : Type u_1))
            (Hom.hom (𝟙 x)).toLinearMap,
        isIntertwining' := ⋯ } =
    𝟙 (of (A.ρ.linHom x.ρ))
have hf : ∀ (x_1 : (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1))) (x_2 : (↑A : Type w)),
  Eq.{u_1 + 1} (α := (↑x : Type u_1))
    ((((Representation.IntertwiningMap.toLinearMap
                  (Hom.hom
                    (ofHom
                      {
                        toLinearMap :=
                          (LinearMap.llcomp k (↑A : Type w) (↑x : Type u_1) (↑x : Type u_1) :
                              (a : (↑x : Type u_1) →ₗ[k] (↑x : Type u_1)) →
                                ((↑A : Type w) →ₗ[k] (↑x : Type u_1)) →ₗ[k] (↑A : Type w) →ₗ[k] (↑x : Type u_1))
                            (Hom.hom (𝟙 x)).toLinearMap,
                        isIntertwining' := sorry : (A.ρ.linHom x.ρ).IntertwiningMap (A.ρ.linHom x.ρ) })) :
                (a : (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1))) → (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1)))
              x_1 :
            (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1))) :
          (a : (↑A : Type w)) → (↑x : Type u_1))
        x_2 :
      (↑x : Type u_1))
    (((((Hom.hom (𝟙 (of (A.ρ.linHom x.ρ)))).toLinearMap :
                (a : (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1))) → (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1)))
              x_1 :
            (↑(of (A.ρ.linHom x.ρ)) : Type (max w u_1))) :
          (a : (↑A : Type w)) → (↑x : Type u_1))
        x_2 :
      (↑x : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A_1 B_1 C_1 : Rep.{w, u, v} k G
A B C : Rep k G
f : tensorObj (𝒞 := instCategory) A B ⟶ C
g : G
⊢ (TensorProduct.curry (Hom.hom f).toLinearMap).flip ∘ₗ (B.ρ : (a : G) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g =
    (A.ρ.linHom C.ρ : (a : G) → ((↑A : Type u) →ₗ[k] (↑C : Type u)) →ₗ[k] (↑A : Type u) →ₗ[k] (↑C : Type u)) g ∘ₗ
      (TensorProduct.curry (Hom.hom f).toLinearMap).flip
have h : ∀ (x : (↑B : Type u)) (y : (↑A : Type u)),
  Eq (α := (↑C : Type u))
    (((((TensorProduct.curry (Hom.hom f).toLinearMap).flip ∘ₗ (B.ρ : (a : G) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g :
                (a : (↑B : Type u)) → (↑A : Type u) →ₗ[k] (↑C : Type u))
              x :
            (↑A : Type u) →ₗ[k] (↑C : Type u)) :
          (a : (↑A : Type u)) → (↑C : Type u))
        y :
      (↑C : Type u))
    (((((A.ρ.linHom C.ρ : (a : G) → ((↑A : Type u) →ₗ[k] (↑C : Type u)) →ₗ[k] (↑A : Type u) →ₗ[k] (↑C : Type u)) g ∘ₗ
                  (TensorProduct.curry (Hom.hom f).toLinearMap).flip :
                (a : (↑B : Type u)) → (↑A : Type u) →ₗ[k] (↑C : Type u))
              x :
            (↑A : Type u) →ₗ[k] (↑C : Type u)) :
          (a : (↑A : Type u)) → (↑C : Type u))
        y :
      (↑C : Type u))
Tactic: ext x y