awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Subrepresentation (goal)
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
⊢ ∀ (g : G) ⦃v : W⦄,
    v ∈ ρ₁.toSubmodule ⊔ ρ₂.toSubmodule →
      Membership.mem (α := W) (ρ₁.toSubmodule ⊔ ρ₂.toSubmodule)
        ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) v : W)
have simp : ∀ (g : G),
  ∀ x₁ ∈ ρ₁.toSubmodule,
    ∀ x₂ ∈ ρ₂.toSubmodule,
      HAdd.hAdd (α := W) (β := W) ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) x₁ : W)
          ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) x₂ : W) ∈
        ρ₁.toSubmodule ⊔ ρ₂.toSubmodule
Tactic: simp only [Submodule.forall_mem_sup, map_add]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Subrepresentation (goal)
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
⊢ ∀ (g : G) ⦃v : W⦄,
    v ∈ ρ₁.toSubmodule ⊓ ρ₂.toSubmodule →
      Membership.mem (α := W) (ρ₁.toSubmodule ⊓ ρ₂.toSubmodule)
        ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) v : W)
have simp : ∀ (g : G) ⦃v : W⦄,
  v ∈ ρ₁.toSubmodule →
    v ∈ ρ₂.toSubmodule →
      Membership.mem (α := W) ρ₁.toSubmodule ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) v : W) ∧
        Membership.mem (α := W) ρ₂.toSubmodule ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) v : W)
Tactic: simp only [Submodule.mem_inf, and_imp]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Subrepresentation (goal)
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • v ∈ σ.toSubmodule.carrier
hy : y • v ∈ σ.toSubmodule.carrier
⊢ (x + y) • v ∈ σ.toSubmodule.carrier
have add : x • v + y • v ∈ σ.toSubmodule.carrier
Tactic: rw [add_smul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Subrepresentation (goal)
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
g : G
a : A
⊢ HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g a) v ∈ σ.toSubmodule.carrier
have single : HSMul.hSMul (β := W) a
    ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) ((ρ.asModuleEquiv : (a : ρ.asModule) → W) v : W) : W) ∈
  σ.toSubmodule.carrier
Tactic: rw [Representation.single_smul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Subrepresentation (goal)
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation ρ
c : A[G]
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
⊢ c • v ∈ σ.toSubmodule.carrier
have zero : HSMul.hSMul (α := A[G]) 0 v ∈ σ.toSubmodule.carrier
Tactic: induction c using MonoidAlgebra.induction_linear with
    | zero => simp [zero_smul]
    | add x y hx hy => rw [add_smul]; exact σ.toSubmodule.add_mem' hx hy
    | single g a =>
      rw [Representation.single_smul]
      exact σ.toSubmodule.smul_mem' a (σ.apply_mem_toSubmodule g hv)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.RepresentationTheory.Subrepresentation (goal)
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation ρ
c : A[G]
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
zero : HSMul.hSMul (α := A[G]) 0 v ∈ σ.toSubmodule.carrier
⊢ c • v ∈ σ.toSubmodule.carrier
have add : ∀ (x y : A[G]) (hx : x • v ∈ σ.toSubmodule.carrier) (hy : y • v ∈ σ.toSubmodule.carrier),
  (x + y) • v ∈ σ.toSubmodule.carrier
Tactic: induction c using MonoidAlgebra.induction_linear with
    | zero => simp [zero_smul]
    | add x y hx hy => rw [add_smul]; exact σ.toSubmodule.add_mem' hx hy
    | single g a =>
      rw [Representation.single_smul]
      exact σ.toSubmodule.smul_mem' a (σ.apply_mem_toSubmodule g hv)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.RepresentationTheory.Subrepresentation (goal)
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation ρ
c : A[G]
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
zero : HSMul.hSMul (α := A[G]) 0 v ∈ σ.toSubmodule.carrier
add :
  ∀ (x y : A[G]) (hx : x • v ∈ σ.toSubmodule.carrier) (hy : y • v ∈ σ.toSubmodule.carrier),
    (x + y) • v ∈ σ.toSubmodule.carrier
⊢ c • v ∈ σ.toSubmodule.carrier
have single : ∀ (g : G) (a : A), HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g a) v ∈ σ.toSubmodule.carrier
Tactic: induction c using MonoidAlgebra.induction_linear with
    | zero => simp [zero_smul]
    | add x y hx hy => rw [add_smul]; exact σ.toSubmodule.add_mem' hx hy
    | single g a =>
      rw [Representation.single_smul]
      exact σ.toSubmodule.smul_mem' a (σ.apply_mem_toSubmodule g hv)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.RepresentationTheory.Subrepresentation (goal)
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
⊢ HSMul.hSMul (α := A[G]) 0 m ∈ σ.toSubmodule.carrier
have zero : 0 ∈ σ.toSubmodule.carrier
Tactic: rw [zero_smul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Subrepresentation (goal)
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • m ∈ σ.toSubmodule.carrier
hy : y • m ∈ σ.toSubmodule.carrier
⊢ (x + y) • m ∈ σ.toSubmodule.carrier
have add : x • m + y • m ∈ σ.toSubmodule.carrier
Tactic: rw [add_smul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Subrepresentation (goal)
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
g : G
a : A
⊢ HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g a) m ∈ σ.toSubmodule.carrier
have single : HSMul.hSMul (α := A[G]) ((algebraMap A A[G] : (a : A) → A[G]) a : A[G])
    (HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g 1) m) ∈
  σ.toSubmodule.carrier
Tactic: rw [← mul_one a, ← smul_eq_mul, ← MonoidAlgebra.smul_single, Algebra.smul_def, mul_smul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Subrepresentation (goal)
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
c : A[G]
m : M
hm : m ∈ σ.toSubmodule.carrier
⊢ c • m ∈ σ.toSubmodule.carrier
have zero : HSMul.hSMul (α := A[G]) 0 m ∈ σ.toSubmodule.carrier
Tactic: induction c using MonoidAlgebra.induction_linear with
    | zero => rw [zero_smul]; exact σ.toSubmodule.zero_mem'
    | add x y hx hy => rw [add_smul]; exact σ.toSubmodule.add_mem' hx hy
    | single g a =>
      rw [← mul_one a, ← smul_eq_mul, ← MonoidAlgebra.smul_single, Algebra.smul_def, mul_smul]
      exact σ.toSubmodule.smul_mem' ((algebraMap A A) a) <| by
        simpa [Representation.ofModule, RestrictScalars.lsmul] using σ.apply_mem_toSubmodule g hm
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.RepresentationTheory.Subrepresentation (goal)
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
c : A[G]
m : M
hm : m ∈ σ.toSubmodule.carrier
zero : HSMul.hSMul (α := A[G]) 0 m ∈ σ.toSubmodule.carrier
⊢ c • m ∈ σ.toSubmodule.carrier
have add : ∀ (x y : A[G]) (hx : x • m ∈ σ.toSubmodule.carrier) (hy : y • m ∈ σ.toSubmodule.carrier),
  (x + y) • m ∈ σ.toSubmodule.carrier
Tactic: induction c using MonoidAlgebra.induction_linear with
    | zero => rw [zero_smul]; exact σ.toSubmodule.zero_mem'
    | add x y hx hy => rw [add_smul]; exact σ.toSubmodule.add_mem' hx hy
    | single g a =>
      rw [← mul_one a, ← smul_eq_mul, ← MonoidAlgebra.smul_single, Algebra.smul_def, mul_smul]
      exact σ.toSubmodule.smul_mem' ((algebraMap A A) a) <| by
        simpa [Representation.ofModule, RestrictScalars.lsmul] using σ.apply_mem_toSubmodule g hm
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.RepresentationTheory.Subrepresentation (goal)
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
σ : Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M)
c : A[G]
m : M
hm : m ∈ σ.toSubmodule.carrier
zero : HSMul.hSMul (α := A[G]) 0 m ∈ σ.toSubmodule.carrier
add :
  ∀ (x y : A[G]) (hx : x • m ∈ σ.toSubmodule.carrier) (hy : y • m ∈ σ.toSubmodule.carrier),
    (x + y) • m ∈ σ.toSubmodule.carrier
⊢ c • m ∈ σ.toSubmodule.carrier
have single : ∀ (g : G) (a : A), HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g a) m ∈ σ.toSubmodule.carrier
Tactic: induction c using MonoidAlgebra.induction_linear with
    | zero => rw [zero_smul]; exact σ.toSubmodule.zero_mem'
    | add x y hx hy => rw [add_smul]; exact σ.toSubmodule.add_mem' hx hy
    | single g a =>
      rw [← mul_one a, ← smul_eq_mul, ← MonoidAlgebra.smul_single, Algebra.smul_def, mul_smul]
      exact σ.toSubmodule.smul_mem' ((algebraMap A A) a) <| by
        simpa [Representation.ofModule, RestrictScalars.lsmul] using σ.apply_mem_toSubmodule g hm
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.RepresentationTheory.Subrepresentation (hypothesis)
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
N : Submodule A[G] ρ.asModule
g : G
w : W
hw : Membership.mem (γ := Submodule A W) { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ } w
x : Module A[G] W := ρ.instModuleMonoidAlgebraAsModule
⊢ Membership.mem (α := W) (γ := Submodule A W) { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
    ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) w : W)
have h : HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g 1) w ∈ N
Tactic: have h : (MonoidAlgebra.single g (1 : A)) • w ∈ N :=
      Submodule.smul_of_tower_mem N _ hw
-- Lean 4 proof step from Mathlib.RepresentationTheory.Subrepresentation (hypothesis)
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
N : Submodule A[G] ρ.asModule
g : G
w : W
hw : Membership.mem (γ := Submodule A W) { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ } w
x : Module A[G] W := ρ.instModuleMonoidAlgebraAsModule
h : HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g 1) w ∈ N
⊢ Membership.mem (α := W) (γ := Submodule A W) { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
    ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) w : W)
have h₁ : Membership.mem (α := W) N
  ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) ((ρ.asModuleEquiv : (a : ρ.asModule) → W) w : W) : W)
Tactic: rw [Representation.single_smul, one_smul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
g : G
X : FDRep k G
⊢ CategoryStruct.comp (Y := X.V) (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g)))
      (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g⁻¹))) =
    𝟙 X.V
have h : ∀ (x : (↑(X.V.obj (P := isFG k)) : Type u)),
  Eq (α := (↑(X.V.obj (P := isFG k)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := X.V)
                (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g)))
                (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g⁻¹))))) :
          (a : (↑X.V.obj : Type u)) → (↑X.V.obj : Type u))
        x :
      (↑(X.V.obj (P := isFG k)) : Type u))
    ((Hom.hom (InducedCategory.Hom.hom (𝟙 X.V)) : (a : (↑X.V.obj : Type u)) → (↑X.V.obj : Type u)) x :
      (↑(X.V.obj (P := isFG k)) : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
g : G
X : FDRep k G
⊢ CategoryStruct.comp (Y := X.V)
      (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g⁻¹)))
      (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g))) =
    𝟙 X.V
have h : ∀ (x : (↑(X.V.obj (P := isFG k)) : Type u)),
  Eq (α := (↑(X.V.obj (P := isFG k)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := X.V)
                (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g⁻¹)))
                (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g))))) :
          (a : (↑X.V.obj : Type u)) → (↑X.V.obj : Type u))
        x :
      (↑(X.V.obj (P := isFG k)) : Type u))
    ((Hom.hom (InducedCategory.Hom.hom (𝟙 X.V)) : (a : (↑X.V.obj : Type u)) → (↑X.V.obj : Type u)) x :
      (↑(X.V.obj (P := isFG k)) : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
⊢ Eq.{u + 2} (α := Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
    (LaxMonoidalFunctor.isoOfComponents (equivApp 1) ⋯ ⋯ ⋯) 1
have h : ∀ (x : FDRep k G) (x_1 : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u)),
  Eq (α := (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (NatTrans.app
                (LaxMonoidalFunctor.Hom.hom (Iso.hom (LaxMonoidalFunctor.isoOfComponents (equivApp 1) sorry sorry sorry))) x)) :
          (a : (↑((forget k G).obj x).obj : Type u)) → (↑((forget k G).obj x).obj : Type u))
        x_1 :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u))
    ((Hom.hom (InducedCategory.Hom.hom (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom 1)) x)) :
          (a : (↑((forget k G).obj x).obj : Type u)) → (↑((forget k G).obj x).obj : Type u))
        x_1 :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x : FDRep k G
x_1 : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u)
⊢ Eq (α := (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (NatTrans.app
                (LaxMonoidalFunctor.Hom.hom (Iso.hom (LaxMonoidalFunctor.isoOfComponents (equivApp 1) ⋯ ⋯ ⋯))) x)) :
          (a : (↑((forget k G).obj x).obj : Type u)) → (↑((forget k G).obj x).obj : Type u))
        x_1 :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u))
    ((Hom.hom (InducedCategory.Hom.hom (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom 1)) x)) :
          (a : (↑((forget k G).obj x).obj : Type u)) → (↑((forget k G).obj x).obj : Type u))
        x_1 :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u))
have h : Eq (α := (↑x.V : Type u)) ((1 : (a : (↑x.V : Type u)) → (↑x.V : Type u)) x_1 : (↑x.V : Type u))
  ((Hom.hom (InducedCategory.Hom.hom (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom 1)) x)) :
        (a : (↑x.V : Type u)) → (↑x.V : Type u))
      x_1 :
    (↑x.V : Type u))
Tactic: simp
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x x_1 : G
⊢ LaxMonoidalFunctor.isoOfComponents (equivApp (x * x_1)) ⋯ ⋯ ⋯ =
    HMul.hMul (α := Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
      (LaxMonoidalFunctor.isoOfComponents (equivApp x) ⋯ ⋯ ⋯) (LaxMonoidalFunctor.isoOfComponents (equivApp x_1) ⋯ ⋯ ⋯)
have h : ∀ (x_2 : FDRep k G)
  (x_3 : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u)),
  Eq (α := (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (NatTrans.app
                (LaxMonoidalFunctor.Hom.hom (Iso.hom (LaxMonoidalFunctor.isoOfComponents (equivApp (x * x_1)) sorry sorry sorry)))
                x_2)) :
          (a : (↑((forget k G).obj x_2).obj : Type u)) → (↑((forget k G).obj x_2).obj : Type u))
        x_3 :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u))
    ((Hom.hom
            ((HMul.hMul (α := Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
                        (LaxMonoidalFunctor.isoOfComponents (equivApp x) sorry sorry sorry)
                        (LaxMonoidalFunctor.isoOfComponents (equivApp x_1) sorry sorry sorry)).hom.hom.app
                x_2).hom :
          (a : (↑((forget k G).obj x_2).obj : Type u)) → (↑((forget k G).obj x_2).obj : Type u))
        x_3 :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x x_1 : G
x_2 : FDRep k G
x_3 : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u)
⊢ Eq (α := (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (NatTrans.app
                (LaxMonoidalFunctor.Hom.hom (Iso.hom (LaxMonoidalFunctor.isoOfComponents (equivApp (x * x_1)) ⋯ ⋯ ⋯)))
                x_2)) :
          (a : (↑((forget k G).obj x_2).obj : Type u)) → (↑((forget k G).obj x_2).obj : Type u))
        x_3 :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u))
    ((Hom.hom
            ((HMul.hMul (α := Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
                        (LaxMonoidalFunctor.isoOfComponents (equivApp x) ⋯ ⋯ ⋯)
                        (LaxMonoidalFunctor.isoOfComponents (equivApp x_1) ⋯ ⋯ ⋯)).hom.hom.app
                x_2).hom :
          (a : (↑((forget k G).obj x_2).obj : Type u)) → (↑((forget k G).obj x_2).obj : Type u))
        x_3 :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u))
have h : Eq (α := (↑x_2.V : Type u))
  ((HMul.hMul (α := (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u)) (β := (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u))
          ((x_2.ρ : (a : G) → (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u)) x : (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u))
          ((x_2.ρ : (a : G) → (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u)) x_1 :
            (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u)) :
        (a : (↑x_2.V : Type u)) → (↑x_2.V : Type u))
      x_3 :
    (↑x_2.V : Type u))
  ((Hom.hom
          ((HMul.hMul (α := Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
                      (LaxMonoidalFunctor.isoOfComponents (equivApp x) sorry sorry sorry)
                      (LaxMonoidalFunctor.isoOfComponents (equivApp x_1) sorry sorry sorry)).hom.hom.app
              x_2).hom :
        (a : (↑x_2.V : Type u)) → (↑x_2.V : Type u))
      x_3 :
    (↑x_2.V : Type u))
Tactic: simp
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
⊢ Eq.{u + 1} (α := (G → k) →ₗ[k] G → k) { toFun := fun (f : G → k) (t : G) ↦ f (t * 1), map_add' := ⋯, map_smul' := ⋯ }
    1
have h : ∀ (x : G → k) (x_1 : G),
  Eq (α := k)
    (({ toFun := fun (f : G → k) (t : G) ↦ f (t * 1), map_add' := sorry, map_smul' := sorry } : (a : G → k) → G → k) x x_1 : k)
    ((1 : (a : G → k) → G → k) x x_1 : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x x_1 : G
⊢ { toFun := fun (f : G → k) (t : G) ↦ f (t * (x * x_1)), map_add' := ⋯, map_smul' := ⋯ } =
    HMul.hMul (α := (G → k) →ₗ[k] G → k)
      { toFun := fun (f : G → k) (t : G) ↦ f (t * x), map_add' := ⋯, map_smul' := ⋯ : (G → k) →ₗ[k] G → k }
      { toFun := fun (f : G → k) (t : G) ↦ f (t * x_1), map_add' := ⋯, map_smul' := ⋯ : (G → k) →ₗ[k] G → k }
have h : ∀ (x_2 : G → k) (x_3 : G),
  Eq (α := k)
    (({ toFun := fun (f : G → k) (t : G) ↦ f (t * (x * x_1)), map_add' := sorry, map_smul' := sorry } : (a : G → k) → G → k) x_2
        x_3 :
      k)
    ((HMul.hMul (α := (G → k) →ₗ[k] G → k)
            { toFun := fun (f : G → k) (t : G) ↦ f (t * x), map_add' := sorry, map_smul' := sorry : (G → k) →ₗ[k] G → k }
            { toFun := fun (f : G → k) (t : G) ↦ f (t * x_1), map_add' := sorry, map_smul' := sorry : (G → k) →ₗ[k] G → k } :
          (a : G → k) → G → k)
        x_2 x_3 :
      k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
⊢ Eq.{u + 1} (α := (G → k) →ₗ[k] G → k)
    { toFun := fun (f : G → k) (t : G) ↦ f (1⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } 1
have h : ∀ (x : G → k) (x_1 : G),
  Eq (α := k)
    (({ toFun := fun (f : G → k) (t : G) ↦ f (1⁻¹ * t), map_add' := sorry, map_smul' := sorry } : (a : G → k) → G → k) x x_1 :
      k)
    ((1 : (a : G → k) → G → k) x x_1 : k)
Tactic: ext