awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ι : Type u_2
inst_2 : Fintype ι
inst_3 : Finite Ω
f : ι → Set Ω
⊢ Eq (α := Measure ((i : ι) → Ω)) (uniformOn (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ f))
    (Measure.pi (α := fun (i : ι) ↦ Ω) fun (i : ι) ↦ uniformOn (f i))
have refine : ∀ (t : (i : ι) → Set Ω) (ht : ∀ (i : ι), MeasurableSet (t i)),
  Eq (α := ENNReal)
    ((uniformOn (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ f) : (a : Set ((i : ι) → Ω)) → ENNReal)
        (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ t) :
      ENNReal)
    (∏ i : ι, ((uniformOn (f i) : Measure Ω) : (a : Set Ω) → ENNReal) (t i) : ENNReal)
Tactic: refine (MeasureTheory.Measure.pi_eq fun t ht ↦ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ι : Type u_2
inst_2 : Fintype ι
inst_3 : Finite Ω
f t : (i : ι) → Set Ω
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Eq (α := ENNReal)
    ((uniformOn (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ f) : (a : Set ((i : ι) → Ω)) → ENNReal)
        (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ t) :
      ENNReal)
    (∏ i : ι, ((uniformOn (f i) : Measure Ω) : (a : Set Ω) → ENNReal) (t i) : ENNReal)
have lift : ∀ (f : (i : ι) → Finset Ω),
  Eq (α := ENNReal)
    ((uniformOn (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ fun (i : ι) ↦ (↑(f i) : Set Ω)) :
          (a : Set ((i : ι) → Ω)) → ENNReal)
        (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ t) :
      ENNReal)
    (∏ i : ι, ((uniformOn ((fun (i : ι) ↦ (↑(f i) : Set Ω)) i) : Measure Ω) : (a : Set Ω) → ENNReal) (t i) : ENNReal)
Tactic: lift f to ι → Finset Ω using by simp [Set.toFinite]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ι : Type u_2
inst_2 : Fintype ι
inst_3 : Finite Ω
t : (i : ι) → Set Ω
ht : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → Finset Ω
⊢ Eq (α := ENNReal)
    ((uniformOn (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ fun (i : ι) ↦ (↑(f i) : Set Ω)) :
          (a : Set ((i : ι) → Ω)) → ENNReal)
        (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ t) :
      ENNReal)
    (∏ i : ι, ((uniformOn ((fun (i : ι) ↦ (↑(f i) : Set Ω)) i) : Measure Ω) : (a : Set Ω) → ENNReal) (t i) : ENNReal)
have lift : ∀ (t : (i : ι) → Finset Ω) (ht : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) ((fun (i : ι) ↦ (↑(t i) : Set Ω)) i)),
  Eq (α := ENNReal)
    ((uniformOn (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ fun (i : ι) ↦ (↑(f i) : Set Ω)) :
          (a : Set ((i : ι) → Ω)) → ENNReal)
        (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ fun (i : ι) ↦ (↑(t i) : Set Ω)) :
      ENNReal)
    (∏ i : ι,
        ((uniformOn ((fun (i : ι) ↦ (↑(f i) : Set Ω)) i) : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : ι) ↦ (↑(t i) : Set Ω)) i) :
      ENNReal)
Tactic: lift t to ι → Finset Ω using by simp [Set.toFinite]
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
⊢ Eq (α := Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} X.V k)
    (Finsupp.lmapDomain k k
      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) 1)) :
        (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V))
    1
have h : ∀ (a a_1 : X.V),
  Eq.{u + 1} (α := k)
    (((Finsupp.lmapDomain k k
                  (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) 1)) :
                    (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V) ∘ₗ
                Finsupp.lsingle a :
              (a : k) → X.V →₀ k)
            1 :
          (a : X.V) → k)
        a_1 :
      k)
    (((1 ∘ₗ Finsupp.lsingle a : (a : k) → X.V →₀ k) 1 : (a : X.V) → k) a_1 : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
x x_1 : G
⊢ Finsupp.lmapDomain k k
      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) (x * x_1))) :
        (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V) =
    HMul.hMul (α := Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} X.V k)
      (Finsupp.lmapDomain k k
        (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x)) :
          (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V))
      (Finsupp.lmapDomain k k
        (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x_1)) :
          (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V))
have h : ∀ (a a_1 : X.V),
  Eq.{u + 1} (α := k)
    (((Finsupp.lmapDomain k k
                  (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) (x * x_1))) :
                    (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V) ∘ₗ
                Finsupp.lsingle a :
              (a : k) → X.V →₀ k)
            1 :
          (a : X.V) → k)
        a_1 :
      k)
    (((HMul.hMul (α := Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} X.V k)
                  (Finsupp.lmapDomain k k
                    (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x)) :
                      (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V))
                  (Finsupp.lmapDomain k k
                    (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x_1)) :
                      (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V)) ∘ₗ
                Finsupp.lsingle a :
              (a : k) → X.V →₀ k)
            1 :
          (a : X.V) → k)
        a_1 :
      k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
f : X ⟶ Y
g : G
⊢ Eq (α := Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} Y.V k)
    (Finsupp.lmapDomain k k
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.hom) :
          (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) Y.V) ∘ₗ
      (linearize k G X : (a : G) → (X.V →₀ k) →ₗ[k] X.V →₀ k) g)
    ((linearize k G Y : (a : G) → (Y.V →₀ k) →ₗ[k] Y.V →₀ k) g ∘ₗ
      Finsupp.lmapDomain k k
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.hom) :
          (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) Y.V))
have h : ∀ (x : X.V) (y : Y.V),
  Eq.{u + 1} (α := k)
    ((((Finsupp.lmapDomain k k
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.hom) :
                      (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) Y.V) ∘ₗ
                  (linearize k G X : (a : G) → (X.V →₀ k) →ₗ[k] X.V →₀ k) g) ∘ₗ
                Finsupp.lsingle x :
              (a : k) → Y.V →₀ k)
            1 :
          (a : Y.V) → k)
        y :
      k)
    (((((linearize k G Y : (a : G) → (Y.V →₀ k) →ₗ[k] Y.V →₀ k) g ∘ₗ
                  Finsupp.lmapDomain k k
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.hom) :
                      (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) Y.V)) ∘ₗ
                Finsupp.lsingle x :
              (a : k) → Y.V →₀ k)
            1 :
          (a : Y.V) → k)
        y :
      k)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
g : G
⊢ Eq (α :=
    k →ₗ[k] Finsupp.{w, u} (Action.V.{w, w + 1, v} (G := G) ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory))) k)
    ((↑(LinearEquiv.symm (Finsupp.uniqueLinearEquiv k k PUnit.unit)) : k →ₗ[k] PUnit.{w + 1} →₀ k) ∘ₗ
      ((trivial k G k : Representation k G k) : (a : G) → k →ₗ[k] k) g)
    ((linearize k G ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory)) :
          (a : G) → ((𝟙_ (Action (Type w) G)).V →₀ k) →ₗ[k] (𝟙_ (Action (Type w) G)).V →₀ k)
        g ∘ₗ
      (↑(LinearEquiv.symm (Finsupp.uniqueLinearEquiv k k PUnit.unit)) : k →ₗ[k] PUnit.{w + 1} →₀ k))
have h : Eq (α := Finsupp.{w, u} (Action.V.{w, w + 1, v} (G := G) ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory))) k)
  (((↑(LinearEquiv.symm (Finsupp.uniqueLinearEquiv k k PUnit.unit)) : k →ₗ[k] PUnit.{w + 1} →₀ k) ∘ₗ
        ((trivial k G k : Representation k G k) : (a : G) → k →ₗ[k] k) g :
      (a : k) → (𝟙_ (Action (Type w) G)).V →₀ k)
    1)
  (((linearize k G ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory)) :
            (a : G) → ((𝟙_ (Action (Type w) G)).V →₀ k) →ₗ[k] (𝟙_ (Action (Type w) G)).V →₀ k)
          g ∘ₗ
        (↑(LinearEquiv.symm (Finsupp.uniqueLinearEquiv k k PUnit.unit)) : k →ₗ[k] PUnit.{w + 1} →₀ k) :
      (a : k) → (𝟙_ (Action (Type w) G)).V →₀ k)
    1)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
g : G
⊢ Eq (α := (Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) →₀ k) →ₗ[k] k)
    ((↑(Finsupp.uniqueLinearEquiv k k PUnit.unit) : (PUnit.{u + 1} →₀ k) →ₗ[k] k) ∘ₗ
      ((linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) :
            Representation k G
              (Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) →₀ k)) :
          (a : G) → ((𝟙_ (Action (Type u) G)).V →₀ k) →ₗ[k] (𝟙_ (Action (Type u) G)).V →₀ k)
        g)
    (((trivial k G k : Representation k G k) : (a : G) → k →ₗ[k] k) g ∘ₗ
      (↑(Finsupp.uniqueLinearEquiv k k PUnit.unit) : (PUnit.{u + 1} →₀ k) →ₗ[k] k))
have h : ∀ (a : Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))),
  Eq (α := k)
    ((((↑(Finsupp.uniqueLinearEquiv k k PUnit.unit) : (PUnit.{u + 1} →₀ k) →ₗ[k] k) ∘ₗ
              ((linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) :
                    Representation k G
                      (Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) →₀ k)) :
                  (a : G) → ((𝟙_ (Action (Type u) G)).V →₀ k) →ₗ[k] (𝟙_ (Action (Type u) G)).V →₀ k)
                g) ∘ₗ
            Finsupp.lsingle a :
          (a : k) → k)
        1 :
      k)
    (((((trivial k G k : Representation k G k) : (a : G) → k →ₗ[k] k) g ∘ₗ
              (↑(Finsupp.uniqueLinearEquiv k k PUnit.unit) : (PUnit.{u + 1} →₀ k) →ₗ[k] k)) ∘ₗ
            Finsupp.lsingle a :
          (a : k) → k)
        1 :
      k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
⊢ Eq (α :=
    IntertwiningMap (V := Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) →₀ k)
      (W := Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) →₀ k)
      (linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)))
      (linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))))
    (comp (ε k G) (η k G)) (IntertwiningMap.id (linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))))
have h : ∀ (a : Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)))
  (a_1 : Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))),
  Eq (α := k)
    (((toLinearMap (comp (ε k G) (η k G)) ∘ₗ Finsupp.lsingle a : (a : k) → (𝟙_ (Action (Type u) G)).V →₀ k) 1 :
          (a : (𝟙_ (Action (Type u) G)).V) → k)
        a_1 :
      k)
    (((toLinearMap (ρ := linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)))
                  (IntertwiningMap.id (linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)))) ∘ₗ
                Finsupp.lsingle a :
              (a : k) → (𝟙_ (Action (Type u) G)).V →₀ k)
            1 :
          (a : (𝟙_ (Action (Type u) G)).V) → k)
        a_1 :
      k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
⊢ Eq (α := IntertwiningMap (trivial k G k) (trivial k G k)) (comp (η k G) (ε k G)) (IntertwiningMap.id (trivial k G k))
have h : Eq (α := k) ((toLinearMap (comp (η k G) (ε k G)) : (a : k) → k) 1 : k)
  ((toLinearMap (ρ := trivial k G k) (IntertwiningMap.id (trivial k G k)) : (a : k) → k) 1 : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
k_1 : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k_1
inst_2 : AddCommGroup V
inst_3 : Module k_1 V
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
σ_1 : Representation k_1 G V
ρ_1 : Representation k_1 G W
X Y Z : Action (Type w) G
k : Type u
inst_6 : CommSemiring k
inst_7 : Module k V
inst_8 : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
⊢ Eq (α :=
    TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k) →ₗ[k]
      Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k)
    ((↑(finsuppTensorFinsupp' k X.V Y.V) : TensorProduct k (X.V →₀ k) (Y.V →₀ k) →ₗ[k] X.V × Y.V →₀ k) ∘ₗ
      (tprod (linearize k G X) (linearize k G Y) :
          (a : G) → TensorProduct k (X.V →₀ k) (Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k))
        g)
    ((linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y) :
          (a : G) → ((X ⊗ Y).V →₀ k) →ₗ[k] (X ⊗ Y).V →₀ k)
        g ∘ₗ
      (↑(finsuppTensorFinsupp' k X.V Y.V) : TensorProduct k (X.V →₀ k) (Y.V →₀ k) →ₗ[k] X.V × Y.V →₀ k))
have a : ∀ (a : X.V) (a_1 : Y.V) (a_2 : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V),
  Eq.{u + 1} (α := k)
    (((((TensorProduct.AlgebraTensorModule.curry
                          ((↑(finsuppTensorFinsupp' k X.V Y.V) :
                              TensorProduct k (X.V →₀ k) (Y.V →₀ k) →ₗ[k] X.V × Y.V →₀ k) ∘ₗ
                            (tprod (linearize k G X) (linearize k G Y) :
                                (a : G) →
                                  TensorProduct k (X.V →₀ k) (Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k))
                              g) ∘ₗ
                        Finsupp.lsingle a :
                      k →ₗ[k]
                        Finsupp.{w, u} Y.V k →ₗ[k]
                          Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k) :
                    (a : k) → (Y.V →₀ k) →ₗ[k] (X ⊗ Y).V →₀ k)
                  1 ∘ₗ
                Finsupp.lsingle a_1 :
              (a : k) → (X ⊗ Y).V →₀ k)
            1 :
          (a : (X ⊗ Y).V) → k)
        a_2 :
      k)
    (((((TensorProduct.AlgebraTensorModule.curry
                          ((linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y) :
                                (a : G) → ((X ⊗ Y).V →₀ k) →ₗ[k] (X ⊗ Y).V →₀ k)
                              g ∘ₗ
                            (↑(finsuppTensorFinsupp' k X.V Y.V) :
                              TensorProduct k (X.V →₀ k) (Y.V →₀ k) →ₗ[k] X.V × Y.V →₀ k)) ∘ₗ
                        Finsupp.lsingle a :
                      k →ₗ[k]
                        Finsupp.{w, u} Y.V k →ₗ[k]
                          Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k) :
                    (a : k) → (Y.V →₀ k) →ₗ[k] (X ⊗ Y).V →₀ k)
                  1 ∘ₗ
                Finsupp.lsingle a_1 :
              (a : k) → (X ⊗ Y).V →₀ k)
            1 :
          (a : (X ⊗ Y).V) → k)
        a_2 :
      k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
G : Type v
inst : Monoid G
X Y : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x : X.V
y : Y.V
r s : k
⊢ Eq (α := Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k)
    ((μ X Y : (a : TensorProduct k (X.V →₀ k) (Y.V →₀ k)) → (X ⊗ Y).V →₀ k)
        (Finsupp.single x r ⊗ₜ[k] Finsupp.single y s) :
      Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k)
    (Finsupp.single (x, y) (r * s) : Finsupp.{w, u} (X.V × Y.V) k)
have h : ∀ (a : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V),
  Eq.{u + 1} (α := k)
    ((((μ X Y : (a : TensorProduct k (X.V →₀ k) (Y.V →₀ k)) → (X ⊗ Y).V →₀ k)
              (Finsupp.single x r ⊗ₜ[k] Finsupp.single y s) :
            Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k) :
          (a : (X ⊗ Y).V) → k)
        a :
      k)
    ((Finsupp.single (x, y) (r * s) : (a : (X ⊗ Y).V) → k) a : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
G : Type v
inst : Monoid G
X Y : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
f : X ⟶ Y
Z : Action (Type w) G
⊢ Eq (α :=
    IntertwiningMap (V := TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Z.V k))
      (tprod (linearize k G X) (linearize k G Z))
      (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z)))
    (comp (μ Y Z) (rTensor (linearize k G Z) (linearizeMap f))) (comp (linearizeMap (f ▷ Z)) (μ X Z))
have h : ∀ (a : X.V) (a_1 : Z.V) (a_2 : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z).V),
  Eq.{u + 1} (α := k)
    (((((TensorProduct.AlgebraTensorModule.curry
                          (toLinearMap (comp (μ Y Z) (rTensor (linearize k G Z) (linearizeMap f)))) ∘ₗ
                        Finsupp.lsingle a :
                      k →ₗ[k]
                        Finsupp.{w, u} Z.V k →ₗ[k]
                          Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z).V k) :
                    (a : k) → (Z.V →₀ k) →ₗ[k] (Y ⊗ Z).V →₀ k)
                  1 ∘ₗ
                Finsupp.lsingle a_1 :
              (a : k) → (Y ⊗ Z).V →₀ k)
            1 :
          (a : (Y ⊗ Z).V) → k)
        a_2 :
      k)
    (((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (comp (linearizeMap (f ▷ Z)) (μ X Z))) ∘ₗ
                        Finsupp.lsingle a :
                      k →ₗ[k]
                        Finsupp.{w, u} Z.V k →ₗ[k]
                          Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z).V k) :
                    (a : k) → (Z.V →₀ k) →ₗ[k] (Y ⊗ Z).V →₀ k)
                  1 ∘ₗ
                Finsupp.lsingle a_1 :
              (a : k) → (Y ⊗ Z).V →₀ k)
            1 :
          (a : (Y ⊗ Z).V) → k)
        a_2 :
      k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
G : Type v
inst : Monoid G
X Y : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
f : X ⟶ Y
Z : Action (Type w) G
⊢ Eq (α :=
    IntertwiningMap (V := TensorProduct k (Finsupp.{w, u} Z.V k) (Finsupp.{w, u} X.V k))
      (tprod (linearize k G Z) (linearize k G X))
      (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Z Y)))
    (comp (μ Z Y) (lTensor (linearize k G Z) (linearizeMap f))) (comp (linearizeMap (Z ◁ f)) (μ Z X))
have h : ∀ (a : Z.V) (a_1 : X.V),
  Eq (α := Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Z Y).V k)
    ((((TensorProduct.AlgebraTensorModule.curry
                    (toLinearMap (comp (μ Z Y) (lTensor (linearize k G Z) (linearizeMap f)))) ∘ₗ
                  Finsupp.lsingle a :
                k →ₗ[k]
                  Finsupp.{w, u} X.V k →ₗ[k]
                    Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Z Y).V k) :
              (a : k) → (X.V →₀ k) →ₗ[k] (Z ⊗ Y).V →₀ k)
            1 ∘ₗ
          Finsupp.lsingle a_1 :
        (a : k) → (Z ⊗ Y).V →₀ k)
      1)
    ((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (comp (linearizeMap (Z ◁ f)) (μ Z X))) ∘ₗ
                  Finsupp.lsingle a :
                k →ₗ[k]
                  Finsupp.{w, u} X.V k →ₗ[k]
                    Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Z Y).V k) :
              (a : k) → (X.V →₀ k) →ₗ[k] (Z ⊗ Y).V →₀ k)
            1 ∘ₗ
          Finsupp.lsingle a_1 :
        (a : k) → (Z ⊗ Y).V →₀ k)
      1)
Tactic: ext : 6
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ Eq (α := Finsupp.{w, u} (X.V × Y.V × Z.V) k)
    ((linearizeMap (Iso.hom (α_ X Y Z)) : (a : (X.V × Y.V) × Z.V →₀ k) → X.V × Y.V × Z.V →₀ k)
        (Finsupp.single ((x, y), z) 1) :
      Finsupp.{w, u} (X.V × Y.V × Z.V) k)
    (Finsupp.single (x, y, z) 1 : Finsupp.{w, u} (X.V × Y.V × Z.V) k)
have h : x =
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
        (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
      ((x, y), z)).1
Tactic: convert! dsimp% linearizeMap_single (α_ X Y Z).hom ((x, y), z) (1 : k)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x : X.V
y : Y.V
z : Z.V
h :
  x =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
          (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
        ((x, y), z)).1
⊢ Eq (α := Finsupp.{w, u} (X.V × Y.V × Z.V) k)
    ((linearizeMap (Iso.hom (α_ X Y Z)) : (a : (X.V × Y.V) × Z.V →₀ k) → X.V × Y.V × Z.V →₀ k)
        (Finsupp.single ((x, y), z) 1) :
      Finsupp.{w, u} (X.V × Y.V × Z.V) k)
    (Finsupp.single (x, y, z) 1 : Finsupp.{w, u} (X.V × Y.V × Z.V) k)
have h₁ : y =
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
          (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
        ((x, y), z)).2.1
Tactic: convert! dsimp% linearizeMap_single (α_ X Y Z).hom ((x, y), z) (1 : k)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x : X.V
y : Y.V
z : Z.V
h :
  x =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
          (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
        ((x, y), z)).1
h₁ :
  y =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
            (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
          ((x, y), z)).2.1
⊢ Eq (α := Finsupp.{w, u} (X.V × Y.V × Z.V) k)
    ((linearizeMap (Iso.hom (α_ X Y Z)) : (a : (X.V × Y.V) × Z.V →₀ k) → X.V × Y.V × Z.V →₀ k)
        (Finsupp.single ((x, y), z) 1) :
      Finsupp.{w, u} (X.V × Y.V × Z.V) k)
    (Finsupp.single (x, y, z) 1 : Finsupp.{w, u} (X.V × Y.V × Z.V) k)
have h₂ : z =
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
          (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
        ((x, y), z)).2.2
Tactic: convert! dsimp% linearizeMap_single (α_ X Y Z).hom ((x, y), z) (1 : k)