[GOAL]
V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
A : Action V G
⊢ ↑A.ρ 1 = 𝟙 A.V
[PROOFSTEP]
rw [MonoidHom.map_one]
[GOAL]
V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
A : Action V G
⊢ 1 = 𝟙 A.V
[PROOFSTEP]
rfl
[GOAL]
V : Type (u + 1)
inst✝ : LargeCategory V
G : GroupCat
A : Action V (MonCat.of ↑G)
g : ↑G
⊢ ↑A.ρ (g⁻¹ * g) = 𝟙 A.V
[PROOFSTEP]
rw [inv_mul_self, ρ_one]
[GOAL]
V : Type (u + 1)
inst✝ : LargeCategory V
G : GroupCat
A : Action V (MonCat.of ↑G)
g : ↑G
⊢ ↑A.ρ (g * g⁻¹) = 𝟙 A.V
[PROOFSTEP]
rw [mul_inv_self, ρ_one]
[GOAL]
V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
M N : Action V G
f : M.V ≅ N.V
comm : autoParam (∀ (g : ↑G), ↑M.ρ g ≫ f.hom = f.hom ≫ ↑N.ρ g) _auto✝
g : ↑G
⊢ ↑N.ρ g ≫ f.inv = f.inv ≫ ↑M.ρ g
[PROOFSTEP]
have w := comm g =≫ f.inv
[GOAL]
V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
M N : Action V G
f : M.V ≅ N.V
comm : autoParam (∀ (g : ↑G), ↑M.ρ g ≫ f.hom = f.hom ≫ ↑N.ρ g) _auto✝
g : ↑G
w : (↑M.ρ g ≫ f.hom) ≫ f.inv = (f.hom ≫ ↑N.ρ g) ≫ f.inv
⊢ ↑N.ρ g ≫ f.inv = f.inv ≫ ↑M.ρ g
[PROOFSTEP]
simp at w 
[GOAL]
V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
M N : Action V G
f : M.V ≅ N.V
comm : autoParam (∀ (g : ↑G), ↑M.ρ g ≫ f.hom = f.hom ≫ ↑N.ρ g) _auto✝
g : ↑G
w : ↑M.ρ g = f.hom ≫ ↑N.ρ g ≫ f.inv
⊢ ↑N.ρ g ≫ f.inv = f.inv ≫ ↑M.ρ g
[PROOFSTEP]
simp [w]
[GOAL]
V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
M N : Action V G
f : M ≅ N
g : ↑G
⊢ ↑N.ρ g = ↑(Iso.conj ((forget V G).mapIso f)) (↑M.ρ g)
[PROOFSTEP]
rw [Iso.conj_apply, Iso.eq_inv_comp]
[GOAL]
V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
M N : Action V G
f : M ≅ N
g : ↑G
⊢ ((forget V G).mapIso f).hom ≫ ↑N.ρ g = ↑M.ρ g ≫ ((forget V G).mapIso f).hom
[PROOFSTEP]
simp [f.hom.comm]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : HasZeroMorphisms V
X Y : Action V G
⊢ ∀ (g : ↑G), ↑X.ρ g ≫ 0 = 0 ≫ ↑Y.ρ g
[PROOFSTEP]
aesop_cat
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
f g : X ⟶ Y
⊢ ∀ (g_1 : ↑G), ↑X.ρ g_1 ≫ (f.hom + g.hom) = (f.hom + g.hom) ≫ ↑Y.ρ g_1
[PROOFSTEP]
simp [f.comm, g.comm]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
⊢ ∀ (a b c : X ⟶ Y), a + b + c = a + (b + c)
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
a✝ b✝ c✝ : X ⟶ Y
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
a✝ b✝ c✝ : X ⟶ Y
⊢ (a✝ + b✝ + c✝).hom = (a✝ + (b✝ + c✝)).hom
[PROOFSTEP]
exact add_assoc _ _ _
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
⊢ ∀ (a : X ⟶ Y), 0 + a = a
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
a✝ : X ⟶ Y
⊢ 0 + a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
a✝ : X ⟶ Y
⊢ (0 + a✝).hom = a✝.hom
[PROOFSTEP]
exact zero_add _
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
⊢ ∀ (a : X ⟶ Y), a + 0 = a
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
a✝ : X ⟶ Y
⊢ a✝ + 0 = a✝
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
a✝ : X ⟶ Y
⊢ (a✝ + 0).hom = a✝.hom
[PROOFSTEP]
exact add_zero _
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
f : X ⟶ Y
⊢ ∀ (g : ↑G), ↑X.ρ g ≫ (-f.hom) = (-f.hom) ≫ ↑Y.ρ g
[PROOFSTEP]
simp [f.comm]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
⊢ ∀ (a : X ⟶ Y), -a + a = 0
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
a✝ : X ⟶ Y
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
a✝ : X ⟶ Y
⊢ (-a✝ + a✝).hom = 0.hom
[PROOFSTEP]
exact add_left_neg _
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
⊢ ∀ (a b : X ⟶ Y), a + b = b + a
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
a✝ b✝ : X ⟶ Y
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
X Y : Action V G
a✝ b✝ : X ⟶ Y
⊢ (a✝ + b✝).hom = (b✝ + a✝).hom
[PROOFSTEP]
exact add_comm _ _
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
⊢ ∀ (P Q R : Action V G) (f f' : P ⟶ Q) (g : Q ⟶ R), (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
P✝ Q✝ R✝ : Action V G
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ (f✝ + f'✝) ≫ g✝ = f✝ ≫ g✝ + f'✝ ≫ g✝
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
P✝ Q✝ R✝ : Action V G
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ ((f✝ + f'✝) ≫ g✝).hom = (f✝ ≫ g✝ + f'✝ ≫ g✝).hom
[PROOFSTEP]
exact Preadditive.add_comp _ _ _ _ _ _
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
⊢ ∀ (P Q R : Action V G) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g'
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
P✝ Q✝ R✝ : Action V G
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ f✝ ≫ (g✝ + g'✝) = f✝ ≫ g✝ + f✝ ≫ g'✝
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : Preadditive V
P✝ Q✝ R✝ : Action V G
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ (f✝ ≫ (g✝ + g'✝)).hom = (f✝ ≫ g✝ + f✝ ≫ g'✝).hom
[PROOFSTEP]
exact Preadditive.comp_add _ _ _ _ _ _
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
r : R
f : X ⟶ Y
⊢ ∀ (g : ↑G), ↑X.ρ g ≫ (r • f.hom) = (r • f.hom) ≫ ↑Y.ρ g
[PROOFSTEP]
simp [f.comm]
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (b : X ⟶ Y), 1 • b = b
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
b✝ : X ⟶ Y
⊢ 1 • b✝ = b✝
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
b✝ : X ⟶ Y
⊢ (1 • b✝).hom = b✝.hom
[PROOFSTEP]
exact one_smul _ _
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (x y : R) (b : X ⟶ Y), (x * y) • b = x • y • b
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
x✝ y✝ : R
b✝ : X ⟶ Y
⊢ (x✝ * y✝) • b✝ = x✝ • y✝ • b✝
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
x✝ y✝ : R
b✝ : X ⟶ Y
⊢ ((x✝ * y✝) • b✝).hom = (x✝ • y✝ • b✝).hom
[PROOFSTEP]
exact mul_smul _ _ _
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (a : R), a • 0 = 0
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
⊢ a✝ • 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
⊢ (a✝ • 0).hom = 0.hom
[PROOFSTEP]
exact smul_zero _
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (a : R) (x y : X ⟶ Y), a • (x + y) = a • x + a • y
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
x✝ y✝ : X ⟶ Y
⊢ a✝ • (x✝ + y✝) = a✝ • x✝ + a✝ • y✝
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
x✝ y✝ : X ⟶ Y
⊢ (a✝ • (x✝ + y✝)).hom = (a✝ • x✝ + a✝ • y✝).hom
[PROOFSTEP]
exact smul_add _ _ _
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (r s : R) (x : X ⟶ Y), (r + s) • x = r • x + s • x
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
r✝ s✝ : R
x✝ : X ⟶ Y
⊢ (r✝ + s✝) • x✝ = r✝ • x✝ + s✝ • x✝
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
r✝ s✝ : R
x✝ : X ⟶ Y
⊢ ((r✝ + s✝) • x✝).hom = (r✝ • x✝ + s✝ • x✝).hom
[PROOFSTEP]
exact add_smul _ _ _
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (x : X ⟶ Y), 0 • x = 0
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
x✝ : X ⟶ Y
⊢ 0 • x✝ = 0
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
x✝ : X ⟶ Y
⊢ (0 • x✝).hom = 0.hom
[PROOFSTEP]
exact zero_smul _ _
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
⊢ ∀ (X Y Z : Action V G) (r : R) (f : X ⟶ Y) (g : Y ⟶ Z), (r • f) ≫ g = r • f ≫ g
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X✝ Y✝ Z✝ : Action V G
r✝ : R
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ (r✝ • f✝) ≫ g✝ = r✝ • f✝ ≫ g✝
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X✝ Y✝ Z✝ : Action V G
r✝ : R
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ ((r✝ • f✝) ≫ g✝).hom = (r✝ • f✝ ≫ g✝).hom
[PROOFSTEP]
exact Linear.smul_comp _ _ _ _ _ _
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
⊢ ∀ (X Y Z : Action V G) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z), f ≫ (r • g) = r • f ≫ g
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X✝ Y✝ Z✝ : Action V G
f✝ : X✝ ⟶ Y✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
⊢ f✝ ≫ (r✝ • g✝) = r✝ • f✝ ≫ g✝
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : MonCat
inst✝² : Preadditive V
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Linear R V
X✝ Y✝ Z✝ : Action V G
f✝ : X✝ ⟶ Y✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
⊢ (f✝ ≫ (r✝ • g✝)).hom = (r✝ • f✝ ≫ g✝).hom
[PROOFSTEP]
exact Linear.comp_smul _ _ _ _ _ _
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X Y Z : Action V G
⊢ (α_ X Y Z).hom.hom = (α_ X.V Y.V Z.V).hom
[PROOFSTEP]
dsimp [Monoidal.transport_associator]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X Y Z : Action V G
⊢ (𝟙 (X.V ⊗ Y.V) ⊗ 𝟙 Z.V) ≫ (α_ X.V Y.V Z.V).hom ≫ (𝟙 X.V ⊗ 𝟙 (Y.V ⊗ Z.V)) = (α_ X.V Y.V Z.V).hom
[PROOFSTEP]
simp
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X Y Z : Action V G
⊢ (α_ X Y Z).inv.hom = (α_ X.V Y.V Z.V).inv
[PROOFSTEP]
dsimp [Monoidal.transport_associator]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X Y Z : Action V G
⊢ ((𝟙 X.V ⊗ 𝟙 (Y.V ⊗ Z.V)) ≫ (α_ X.V Y.V Z.V).inv) ≫ (𝟙 (X.V ⊗ Y.V) ⊗ 𝟙 Z.V) = (α_ X.V Y.V Z.V).inv
[PROOFSTEP]
simp
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X : Action V G
⊢ (λ_ X).hom.hom = (λ_ X.V).hom
[PROOFSTEP]
dsimp [Monoidal.transport_leftUnitor]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X : Action V G
⊢ ((𝟙 (𝟙_ V) ⊗ 𝟙 X.V) ≫ (λ_ X.V).hom) ≫ 𝟙 X.V = (λ_ X.V).hom
[PROOFSTEP]
simp
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X : Action V G
⊢ (λ_ X).inv.hom = (λ_ X.V).inv
[PROOFSTEP]
dsimp [Monoidal.transport_leftUnitor]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X : Action V G
⊢ 𝟙 X.V ≫ (λ_ X.V).inv ≫ (𝟙 (𝟙_ V) ⊗ 𝟙 X.V) = (λ_ X.V).inv
[PROOFSTEP]
simp
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X : Action V G
⊢ (ρ_ X).hom.hom = (ρ_ X.V).hom
[PROOFSTEP]
dsimp [Monoidal.transport_rightUnitor]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X : Action V G
⊢ ((𝟙 X.V ⊗ 𝟙 (𝟙_ V)) ≫ (ρ_ X.V).hom) ≫ 𝟙 X.V = (ρ_ X.V).hom
[PROOFSTEP]
simp
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X : Action V G
⊢ (ρ_ X).inv.hom = (ρ_ X.V).inv
[PROOFSTEP]
dsimp [Monoidal.transport_rightUnitor]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X : Action V G
⊢ 𝟙 X.V ≫ (ρ_ X.V).inv ≫ (𝟙 X.V ⊗ 𝟙 (𝟙_ V)) = (ρ_ X.V).inv
[PROOFSTEP]
simp
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X : V
f : 𝟙_ V ≅ X
x✝ : ↑G
⊢ ↑(𝟙_ (Action V G)).ρ x✝ ≫ f.hom = f.hom ≫ ↑{ V := X, ρ := 1 }.ρ x✝
[PROOFSTEP]
simp only [MonoidHom.one_apply, End.one_def, Category.id_comp f.hom, tensorUnit_rho, MonCat.oneHom_apply, MonCat.one_of,
  Category.comp_id]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
⊢ Faithful (forgetMonoidal V G).toLaxMonoidalFunctor.toFunctor
[PROOFSTEP]
change Faithful (forget V G)
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
⊢ Faithful (forget V G)
[PROOFSTEP]
infer_instance
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
inst✝ : BraidedCategory V
X Y : Action V G
g : ↑G
⊢ ↑(X ⊗ Y).ρ g ≫
      (β_ (((CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).inverse.obj X).obj PUnit.unit)
          (((CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).inverse.obj Y).obj PUnit.unit)).hom =
    (β_ (((CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).inverse.obj X).obj PUnit.unit)
          (((CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).inverse.obj Y).obj PUnit.unit)).hom ≫
      ↑(Y ⊗ X).ρ g
[PROOFSTEP]
simp [FunctorCategoryEquivalence.inverse]
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
inst✝ : BraidedCategory V
⊢ ∀ (X Y : Action V G),
    LaxMonoidalFunctor.μ (forgetMonoidal V G).toLaxMonoidalFunctor X Y ≫
        (forgetMonoidal V G).toLaxMonoidalFunctor.toFunctor.map
          ((fun X Y =>
                mkIso
                  (β_
                    (((CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).inverse.obj X).obj PUnit.unit)
                    (((CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).inverse.obj Y).obj
                      PUnit.unit)))
              X Y).hom =
      (β_ ((forgetMonoidal V G).toLaxMonoidalFunctor.toFunctor.obj X)
            ((forgetMonoidal V G).toLaxMonoidalFunctor.toFunctor.obj Y)).hom ≫
        LaxMonoidalFunctor.μ (forgetMonoidal V G).toLaxMonoidalFunctor Y X
[PROOFSTEP]
aesop_cat
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
inst✝ : BraidedCategory V
⊢ Faithful (forgetBraided V G).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor
[PROOFSTEP]
change Faithful (forget V G)
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
inst✝ : BraidedCategory V
⊢ Faithful (forget V G)
[PROOFSTEP]
infer_instance
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
⊢ IsEquivalence (functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor
[PROOFSTEP]
change IsEquivalence (Action.functorCategoryEquivalence _ _).functor
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
⊢ IsEquivalence (functorCategoryEquivalence V G).functor
[PROOFSTEP]
infer_instance
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ NatTrans.app (LaxMonoidalFunctor.μ (functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor A B) PUnit.unit =
    𝟙
      (((functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj A ⊗
            (functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj B).obj
        PUnit.unit)
[PROOFSTEP]
dsimp only [functorCategoryMonoidalEquivalence]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ NatTrans.app
      (LaxMonoidalFunctor.μ
        (Monoidal.fromTransported
            (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G))).toLaxMonoidalFunctor
        A B)
      PUnit.unit =
    𝟙
      (((Monoidal.fromTransported
                      (CategoryTheory.Equivalence.symm
                        (functorCategoryEquivalence V G))).toLaxMonoidalFunctor.toFunctor.obj
              A ⊗
            (Monoidal.fromTransported
                      (CategoryTheory.Equivalence.symm
                        (functorCategoryEquivalence V G))).toLaxMonoidalFunctor.toFunctor.obj
              B).obj
        PUnit.unit)
[PROOFSTEP]
simp only [Monoidal.fromTransported_toLaxMonoidalFunctor_μ, NatTrans.comp_app]
  -- porting note: Lean3 was able to see through some defeq, as the mathlib3 proof was
    --   show (𝟙 A.V ⊗ 𝟙 B.V) ≫ 𝟙 (A.V ⊗ B.V) ≫ (𝟙 A.V ⊗ 𝟙 B.V) = 𝟙 (A.V ⊗ B.V)
    --   simp only [monoidal_category.tensor_id, category.comp_id]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ NatTrans.app
        (NatTrans.app (Equivalence.unit (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
          ((Functor.asEquivalence
                    (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).functor).inverse.obj
              A ⊗
            (Functor.asEquivalence
                    (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).functor).inverse.obj
              B))
        PUnit.unit ≫
      NatTrans.app
          (inv
            ((Functor.asEquivalence
                    (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).functor).inverse.map
              ((CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).functor.map
                (NatTrans.app (Equivalence.unitInv (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
                    ((Functor.asEquivalence
                            (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).functor).inverse.obj
                      A) ⊗
                  NatTrans.app (Equivalence.unitInv (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
                    ((Functor.asEquivalence
                            (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).functor).inverse.obj
                      B)))))
          PUnit.unit ≫
        NatTrans.app
          ((Functor.asEquivalence
                  (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).functor).inverse.map
            ((CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).functor.map
              ((CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).inverse.map
                  (NatTrans.app (Equivalence.counit (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
                    A) ⊗
                (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)).inverse.map
                  (NatTrans.app (Equivalence.counit (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
                    B))))
          PUnit.unit =
    𝟙
      (((Monoidal.fromTransported
                      (CategoryTheory.Equivalence.symm
                        (functorCategoryEquivalence V G))).toLaxMonoidalFunctor.toFunctor.obj
              A ⊗
            (Monoidal.fromTransported
                      (CategoryTheory.Equivalence.symm
                        (functorCategoryEquivalence V G))).toLaxMonoidalFunctor.toFunctor.obj
              B).obj
        PUnit.unit)
[PROOFSTEP]
dsimp [Equivalence.unit]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ 𝟙
        (((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.obj A).obj PUnit.unit ⊗
          ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.obj B).obj PUnit.unit) ≫
      NatTrans.app
          (inv
            ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.map
              (FunctorCategoryEquivalence.inverse.map
                (NatTrans.app (Equivalence.unitInv (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
                    ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.obj A) ⊗
                  NatTrans.app (Equivalence.unitInv (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
                    ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.obj B)))))
          PUnit.unit ≫
        NatTrans.app
          ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.map
            (FunctorCategoryEquivalence.inverse.map
              (FunctorCategoryEquivalence.functor.map
                  (NatTrans.app (Equivalence.counit (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
                    A) ⊗
                FunctorCategoryEquivalence.functor.map
                  (NatTrans.app (Equivalence.counit (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
                    B))))
          PUnit.unit =
    𝟙
      (((Monoidal.fromTransported
                      (CategoryTheory.Equivalence.symm
                        (functorCategoryEquivalence V G))).toLaxMonoidalFunctor.toFunctor.obj
              A).obj
          PUnit.unit ⊗
        ((Monoidal.fromTransported
                      (CategoryTheory.Equivalence.symm
                        (functorCategoryEquivalence V G))).toLaxMonoidalFunctor.toFunctor.obj
              B).obj
          PUnit.unit)
[PROOFSTEP]
erw [Category.id_comp]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ NatTrans.app
        (inv
          ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.map
            (FunctorCategoryEquivalence.inverse.map
              (NatTrans.app (Equivalence.unitInv (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
                  ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.obj A) ⊗
                NatTrans.app (Equivalence.unitInv (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
                  ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.obj B)))))
        PUnit.unit ≫
      NatTrans.app
        ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.map
          (FunctorCategoryEquivalence.inverse.map
            (FunctorCategoryEquivalence.functor.map
                (NatTrans.app (Equivalence.counit (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
                  A) ⊗
              FunctorCategoryEquivalence.functor.map
                (NatTrans.app (Equivalence.counit (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
                  B))))
        PUnit.unit =
    𝟙
      (((Monoidal.fromTransported
                      (CategoryTheory.Equivalence.symm
                        (functorCategoryEquivalence V G))).toLaxMonoidalFunctor.toFunctor.obj
              A).obj
          PUnit.unit ⊗
        ((Monoidal.fromTransported
                      (CategoryTheory.Equivalence.symm
                        (functorCategoryEquivalence V G))).toLaxMonoidalFunctor.toFunctor.obj
              B).obj
          PUnit.unit)
[PROOFSTEP]
rw [NatIso.isIso_inv_app, IsIso.inv_comp_eq]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ NatTrans.app
      ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.map
        (FunctorCategoryEquivalence.inverse.map
          (FunctorCategoryEquivalence.functor.map
              (NatTrans.app (Equivalence.counit (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G))) A) ⊗
            FunctorCategoryEquivalence.functor.map
              (NatTrans.app (Equivalence.counit (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
                B))))
      PUnit.unit =
    NatTrans.app
        ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.map
          (FunctorCategoryEquivalence.inverse.map
            (NatTrans.app (Equivalence.unitInv (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
                ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.obj A) ⊗
              NatTrans.app (Equivalence.unitInv (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
                ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.obj B))))
        PUnit.unit ≫
      𝟙
        (((Monoidal.fromTransported
                        (CategoryTheory.Equivalence.symm
                          (functorCategoryEquivalence V G))).toLaxMonoidalFunctor.toFunctor.obj
                A).obj
            PUnit.unit ⊗
          ((Monoidal.fromTransported
                        (CategoryTheory.Equivalence.symm
                          (functorCategoryEquivalence V G))).toLaxMonoidalFunctor.toFunctor.obj
                B).obj
            PUnit.unit)
[PROOFSTEP]
erw [MonoidalCategory.tensor_id]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ NatTrans.app
      ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.map
        (FunctorCategoryEquivalence.inverse.map
          (𝟙
            (FunctorCategoryEquivalence.functor.obj
                (FunctorCategoryEquivalence.inverse.obj
                  ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.obj A)) ⊗
              FunctorCategoryEquivalence.functor.obj
                (FunctorCategoryEquivalence.inverse.obj
                  ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.obj B))))))
      PUnit.unit =
    NatTrans.app
        ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.map
          (FunctorCategoryEquivalence.inverse.map
            (𝟙
              (FunctorCategoryEquivalence.functor.obj
                  (FunctorCategoryEquivalence.inverse.obj
                    ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.obj A)) ⊗
                FunctorCategoryEquivalence.functor.obj
                  (FunctorCategoryEquivalence.inverse.obj
                    ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.obj B))))))
        PUnit.unit ≫
      𝟙
        (((Monoidal.fromTransported
                        (CategoryTheory.Equivalence.symm
                          (functorCategoryEquivalence V G))).toLaxMonoidalFunctor.toFunctor.obj
                A).obj
            PUnit.unit ⊗
          ((Monoidal.fromTransported
                        (CategoryTheory.Equivalence.symm
                          (functorCategoryEquivalence V G))).toLaxMonoidalFunctor.toFunctor.obj
                B).obj
            PUnit.unit)
[PROOFSTEP]
erw [(functorCategoryEquivalence V G).inverse.map_id, (functorCategoryEquivalence V G).functor.map_id, Category.id_comp]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ NatTrans.app
      (𝟙
        ((functorCategoryEquivalence V G).functor.obj
          (FunctorCategoryEquivalence.inverse.obj
            (FunctorCategoryEquivalence.functor.obj
                (FunctorCategoryEquivalence.inverse.obj
                  ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.obj A)) ⊗
              FunctorCategoryEquivalence.functor.obj
                (FunctorCategoryEquivalence.inverse.obj
                  ((Functor.asEquivalence FunctorCategoryEquivalence.inverse).inverse.obj B))))))
      PUnit.unit =
    𝟙
      (((Monoidal.fromTransported
                      (CategoryTheory.Equivalence.symm
                        (functorCategoryEquivalence V G))).toLaxMonoidalFunctor.toFunctor.obj
              A).obj
          PUnit.unit ⊗
        ((Monoidal.fromTransported
                      (CategoryTheory.Equivalence.symm
                        (functorCategoryEquivalence V G))).toLaxMonoidalFunctor.toFunctor.obj
              B).obj
          PUnit.unit)
[PROOFSTEP]
rfl
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ NatTrans.app (MonoidalFunctor.μIso (functorCategoryMonoidalEquivalence V G) A B).inv PUnit.unit =
    𝟙 (((functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj (A ⊗ B)).obj PUnit.unit)
[PROOFSTEP]
rw [← NatIso.app_inv, ← IsIso.Iso.inv_hom]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ inv ((MonoidalFunctor.μIso (functorCategoryMonoidalEquivalence V G) A B).app PUnit.unit).hom =
    𝟙 (((functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj (A ⊗ B)).obj PUnit.unit)
[PROOFSTEP]
refine' IsIso.inv_eq_of_hom_inv_id _
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
A B : Action V G
⊢ ((MonoidalFunctor.μIso (functorCategoryMonoidalEquivalence V G) A B).app PUnit.unit).hom ≫
      𝟙 (((functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj (A ⊗ B)).obj PUnit.unit) =
    𝟙
      (((functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj A ⊗
            (functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.toFunctor.obj B).obj
        PUnit.unit)
[PROOFSTEP]
rw [Category.comp_id, NatIso.app_hom, MonoidalFunctor.μIso_hom, functorCategoryMonoidalEquivalence.μ_app]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
⊢ NatTrans.app (functorCategoryMonoidalEquivalence V G).toLaxMonoidalFunctor.ε PUnit.unit =
    𝟙 ((𝟙_ (SingleObj ↑G ⥤ V)).obj PUnit.unit)
[PROOFSTEP]
dsimp only [functorCategoryMonoidalEquivalence]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
⊢ NatTrans.app
      (Monoidal.fromTransported
            (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G))).toLaxMonoidalFunctor.ε
      PUnit.unit =
    𝟙 ((𝟙_ (SingleObj ↑G ⥤ V)).obj PUnit.unit)
[PROOFSTEP]
simp only [Monoidal.fromTransported_toLaxMonoidalFunctor_ε]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
⊢ NatTrans.app
      (NatTrans.app (Equivalence.unit (CategoryTheory.Equivalence.symm (functorCategoryEquivalence V G)))
        (𝟙_ (SingleObj ↑G ⥤ V)))
      PUnit.unit =
    𝟙 ((𝟙_ (SingleObj ↑G ⥤ V)).obj PUnit.unit)
[PROOFSTEP]
rfl
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
inst✝ : RightRigidCategory V
⊢ RightRigidCategory (SingleObj ↑((forget₂ GroupCat MonCat).obj H) ⥤ V)
[PROOFSTEP]
change RightRigidCategory (SingleObj H ⥤ V)
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
inst✝ : RightRigidCategory V
⊢ RightRigidCategory (SingleObj ↑H ⥤ V)
[PROOFSTEP]
infer_instance
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
inst✝ : LeftRigidCategory V
⊢ LeftRigidCategory (SingleObj ↑((forget₂ GroupCat MonCat).obj H) ⥤ V)
[PROOFSTEP]
change LeftRigidCategory (SingleObj H ⥤ V)
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
inst✝ : LeftRigidCategory V
⊢ LeftRigidCategory (SingleObj ↑H ⥤ V)
[PROOFSTEP]
infer_instance
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
inst✝ : RigidCategory V
⊢ RigidCategory (SingleObj ↑((forget₂ GroupCat MonCat).obj H) ⥤ V)
[PROOFSTEP]
change RigidCategory (SingleObj H ⥤ V)
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
inst✝ : RigidCategory V
⊢ RigidCategory (SingleObj ↑H ⥤ V)
[PROOFSTEP]
infer_instance
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
X : Action V ((forget₂ GroupCat MonCat).obj H)
inst✝ : RightRigidCategory V
h : ↑H
⊢ ↑Xᘁ.ρ h = ↑X.ρ h⁻¹ᘁ
[PROOFSTEP]
rw [← SingleObj.inv_as_inv]
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
X : Action V ((forget₂ GroupCat MonCat).obj H)
inst✝ : RightRigidCategory V
h : ↑H
⊢ ↑Xᘁ.ρ h = ↑X.ρ (inv h)ᘁ
case x
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
X : Action V ((forget₂ GroupCat MonCat).obj H)
inst✝ : RightRigidCategory V
h : ↑H
⊢ SingleObj H.1
case y
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
X : Action V ((forget₂ GroupCat MonCat).obj H)
inst✝ : RightRigidCategory V
h : ↑H
⊢ SingleObj H.1
[PROOFSTEP]
rfl
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
X : Action V ((forget₂ GroupCat MonCat).obj H)
inst✝ : LeftRigidCategory V
h : ↑H
⊢ ↑(ᘁX).ρ h = ᘁ↑X.ρ h⁻¹
[PROOFSTEP]
rw [← SingleObj.inv_as_inv]
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
X : Action V ((forget₂ GroupCat MonCat).obj H)
inst✝ : LeftRigidCategory V
h : ↑H
⊢ ↑(ᘁX).ρ h = ᘁ↑X.ρ (inv h)
case x
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
X : Action V ((forget₂ GroupCat MonCat).obj H)
inst✝ : LeftRigidCategory V
h : ↑H
⊢ SingleObj H.1
case y
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
X : Action V ((forget₂ GroupCat MonCat).obj H)
inst✝ : LeftRigidCategory V
h : ↑H
⊢ SingleObj H.1
[PROOFSTEP]
rfl
[GOAL]
V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
X✝ Y✝ : V
f : X✝ ⟶ Y✝
x✝ : ↑(MonCat.of PUnit)
⊢ ↑((fun X => { V := X, ρ := 1 }) X✝).ρ PUnit.unit ≫ f = f ≫ ↑((fun X => { V := X, ρ := 1 }) Y✝).ρ PUnit.unit
[PROOFSTEP]
simp
[GOAL]
V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
X : Action V (MonCat.of PUnit)
x✝ : ↑(MonCat.of PUnit)
⊢ ↑((𝟭 (Action V (MonCat.of PUnit))).obj X).ρ PUnit.unit ≫ (Iso.refl ((𝟭 (Action V (MonCat.of PUnit))).obj X).V).hom =
    (Iso.refl ((𝟭 (Action V (MonCat.of PUnit))).obj X).V).hom ≫
      ↑((forget V (MonCat.of PUnit) ⋙
                  CategoryTheory.Functor.mk { obj := fun X => { V := X, ρ := 1 }, map := fun {X Y} f => Hom.mk f }).obj
              X).ρ
        PUnit.unit
[PROOFSTEP]
simp only [MonCat.oneHom_apply, MonCat.one_of, End.one_def, id_eq, Functor.comp_obj, forget_obj, Iso.refl_hom,
  Category.comp_id]
[GOAL]
V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
X : Action V (MonCat.of PUnit)
x✝ : ↑(MonCat.of PUnit)
⊢ ↑((𝟭 (Action V (MonCat.of PUnit))).obj X).ρ PUnit.unit = 𝟙 ((𝟭 (Action V (MonCat.of PUnit))).obj X).V
[PROOFSTEP]
exact ρ_one X
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G✝ H✝ : MonCat
f : G✝ ⟶ H✝
R : Type u_1
inst✝² : Semiring R
G H : Type u
inst✝¹ : Monoid G
inst✝ : MulAction G H
⊢ MulAction (↑(MonCat.of G)) H
[PROOFSTEP]
assumption
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝² : Semiring R
ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i => ofMulAction G (F i))
g : ↑(MonCat.of G)
⊢ (↑s.pt.ρ g ≫ fun x i => Hom.hom (NatTrans.app s.π { as := i }) x) =
    (fun x i => Hom.hom (NatTrans.app s.π { as := i }) x) ≫
      ↑{ pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i => Hom.mk fun x => x i.as }.pt.ρ g
[PROOFSTEP]
ext x
[GOAL]
case h
V : Type (u + 1)
inst✝³ : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝² : Semiring R
ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i => ofMulAction G (F i))
g : ↑(MonCat.of G)
x : s.pt.V
⊢ (↑s.pt.ρ g ≫ fun x i => Hom.hom (NatTrans.app s.π { as := i }) x) x =
    ((fun x i => Hom.hom (NatTrans.app s.π { as := i }) x) ≫
        ↑{ pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i => Hom.mk fun x => x i.as }.pt.ρ g)
      x
[PROOFSTEP]
funext j
[GOAL]
case h.h
V : Type (u + 1)
inst✝³ : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝² : Semiring R
ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i => ofMulAction G (F i))
g : ↑(MonCat.of G)
x : s.pt.V
j : ι
⊢ (↑s.pt.ρ g ≫ fun x i => Hom.hom (NatTrans.app s.π { as := i }) x) x j =
    ((fun x i => Hom.hom (NatTrans.app s.π { as := i }) x) ≫
        ↑{ pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i => Hom.mk fun x => x i.as }.pt.ρ g)
      x j
[PROOFSTEP]
exact congr_fun ((s.π.app ⟨j⟩).comm g) x
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
G✝ H : MonCat
f✝ : G✝ ⟶ H
R : Type u_1
inst✝² : Semiring R
ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i => ofMulAction G (F i))
f : s.pt ⟶ { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i => Hom.mk fun x => x i.as }.pt
h :
  ∀ (j : Discrete ι),
    f ≫
        NatTrans.app { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i => Hom.mk fun x => x i.as }.π
          j =
      NatTrans.app s.π j
⊢ f = (fun s => Hom.mk fun x i => Hom.hom (NatTrans.app s.π { as := i }) x) s
[PROOFSTEP]
ext x
[GOAL]
case h.h
V : Type (u + 1)
inst✝³ : LargeCategory V
G✝ H : MonCat
f✝ : G✝ ⟶ H
R : Type u_1
inst✝² : Semiring R
ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i => ofMulAction G (F i))
f : s.pt ⟶ { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i => Hom.mk fun x => x i.as }.pt
h :
  ∀ (j : Discrete ι),
    f ≫
        NatTrans.app { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i => Hom.mk fun x => x i.as }.π
          j =
      NatTrans.app s.π j
x : s.pt.V
⊢ Hom.hom f x = Hom.hom ((fun s => Hom.mk fun x i => Hom.hom (NatTrans.app s.π { as := i }) x) s) x
[PROOFSTEP]
funext j
[GOAL]
case h.h.h
V : Type (u + 1)
inst✝³ : LargeCategory V
G✝ H : MonCat
f✝ : G✝ ⟶ H
R : Type u_1
inst✝² : Semiring R
ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i => ofMulAction G (F i))
f : s.pt ⟶ { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i => Hom.mk fun x => x i.as }.pt
h :
  ∀ (j : Discrete ι),
    f ≫
        NatTrans.app { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i => Hom.mk fun x => x i.as }.π
          j =
      NatTrans.app s.π j
x : s.pt.V
j : ι
⊢ Hom.hom f x j = Hom.hom ((fun s => Hom.mk fun x i => Hom.hom (NatTrans.app s.π { as := i }) x) s) x j
[PROOFSTEP]
dsimp at *
[GOAL]
case h.h.h
V : Type (u + 1)
inst✝³ : LargeCategory V
G✝ H : MonCat
f✝ : G✝ ⟶ H
R : Type u_1
inst✝² : Semiring R
ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i => ofMulAction G (F i))
f : s.pt ⟶ { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i => Hom.mk fun x => x i.as }.pt
h : ∀ (j : Discrete ι), (f ≫ Hom.mk fun x => x j.as) = NatTrans.app s.π j
x : s.pt.V
j : ι
⊢ Hom.hom f x j = Hom.hom (NatTrans.app s.π { as := j }) x
[PROOFSTEP]
rw [← h ⟨j⟩]
[GOAL]
case h.h.h
V : Type (u + 1)
inst✝³ : LargeCategory V
G✝ H : MonCat
f✝ : G✝ ⟶ H
R : Type u_1
inst✝² : Semiring R
ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i => ofMulAction G (F i))
f : s.pt ⟶ { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i => Hom.mk fun x => x i.as }.pt
h : ∀ (j : Discrete ι), (f ≫ Hom.mk fun x => x j.as) = NatTrans.app s.π j
x : s.pt.V
j : ι
⊢ Hom.hom f x j = Hom.hom (f ≫ Hom.mk fun x => x { as := j }.as) x
[PROOFSTEP]
rfl
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
g : G
⊢ (↑(leftRegular G ⊗ X).ρ g ≫ fun g => (g.fst, ↑X.ρ g.fst⁻¹ g.snd)) =
    (fun g => (g.fst, ↑X.ρ g.fst⁻¹ g.snd)) ≫ ↑(leftRegular G ⊗ { V := X.V, ρ := 1 }).ρ g
[PROOFSTEP]
funext ⟨(x₁ : G), (x₂ : X.V)⟩
[GOAL]
case h
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
g x₁ : G
x₂ : X.V
⊢ (↑(leftRegular G ⊗ X).ρ g ≫ fun g => (g.fst, ↑X.ρ g.fst⁻¹ g.snd)) (x₁, x₂) =
    ((fun g => (g.fst, ↑X.ρ g.fst⁻¹ g.snd)) ≫ ↑(leftRegular G ⊗ { V := X.V, ρ := 1 }).ρ g) (x₁, x₂)
[PROOFSTEP]
refine' Prod.ext rfl _
[GOAL]
case h
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
g x₁ : G
x₂ : X.V
⊢ ((↑(leftRegular G ⊗ X).ρ g ≫ fun g => (g.fst, ↑X.ρ g.fst⁻¹ g.snd)) (x₁, x₂)).snd =
    (((fun g => (g.fst, ↑X.ρ g.fst⁻¹ g.snd)) ≫ ↑(leftRegular G ⊗ { V := X.V, ρ := 1 }).ρ g) (x₁, x₂)).snd
[PROOFSTEP]
change (X.ρ ((g * x₁)⁻¹ : G) * X.ρ g) x₂ = X.ρ _ _
[GOAL]
case h
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
g x₁ : G
x₂ : X.V
⊢ (↑X.ρ (g * x₁)⁻¹ * ↑X.ρ g) x₂ = ↑X.ρ (x₁, x₂).fst⁻¹ (x₁, x₂).snd
[PROOFSTEP]
rw [mul_inv_rev, ← X.ρ.map_mul, inv_mul_cancel_right]
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
g : G
⊢ (↑(leftRegular G ⊗ { V := X.V, ρ := 1 }).ρ g ≫ fun g => (g.fst, ↑X.ρ g.fst g.snd)) =
    (fun g => (g.fst, ↑X.ρ g.fst g.snd)) ≫ ↑(leftRegular G ⊗ X).ρ g
[PROOFSTEP]
funext ⟨(x₁ : G), (x₂ : X.V)⟩
[GOAL]
case h
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
g x₁ : G
x₂ : X.V
⊢ (↑(leftRegular G ⊗ { V := X.V, ρ := 1 }).ρ g ≫ fun g => (g.fst, ↑X.ρ g.fst g.snd)) (x₁, x₂) =
    ((fun g => (g.fst, ↑X.ρ g.fst g.snd)) ≫ ↑(leftRegular G ⊗ X).ρ g) (x₁, x₂)
[PROOFSTEP]
refine' Prod.ext rfl _
[GOAL]
case h
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
g x₁ : G
x₂ : X.V
⊢ ((↑(leftRegular G ⊗ { V := X.V, ρ := 1 }).ρ g ≫ fun g => (g.fst, ↑X.ρ g.fst g.snd)) (x₁, x₂)).snd =
    (((fun g => (g.fst, ↑X.ρ g.fst g.snd)) ≫ ↑(leftRegular G ⊗ X).ρ g) (x₁, x₂)).snd
[PROOFSTEP]
erw [tensor_rho, tensor_rho]
[GOAL]
case h
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
g x₁ : G
x₂ : X.V
⊢ (((↑(leftRegular G).ρ g ⊗ ↑{ V := X.V, ρ := 1 }.ρ g) ≫ fun g => (g.fst, ↑X.ρ g.fst g.snd)) (x₁, x₂)).snd =
    (((fun g => (g.fst, ↑X.ρ g.fst g.snd)) ≫ (↑(leftRegular G).ρ g ⊗ ↑X.ρ g)) (x₁, x₂)).snd
[PROOFSTEP]
dsimp
[GOAL]
case h
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
g x₁ : G
x₂ : X.V
⊢ ↑X.ρ (↑(leftRegular G).ρ g x₁) x₂ = ↑X.ρ g (↑X.ρ x₁ x₂)
[PROOFSTEP]
rw [leftRegular_ρ_apply]
[GOAL]
case h
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
g x₁ : G
x₂ : X.V
⊢ ↑X.ρ (g • x₁) x₂ = ↑X.ρ g (↑X.ρ x₁ x₂)
[PROOFSTEP]
erw [map_mul]
[GOAL]
case h
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
g x₁ : G
x₂ : X.V
⊢ (↑X.ρ g * ↑X.ρ x₁) x₂ = ↑X.ρ g (↑X.ρ x₁ x₂)
[PROOFSTEP]
rfl
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
⊢ ((Hom.mk fun g => (g.fst, ↑X.ρ g.fst⁻¹ g.snd)) ≫ Hom.mk fun g => (g.fst, ↑X.ρ g.fst g.snd)) = 𝟙 (leftRegular G ⊗ X)
[PROOFSTEP]
apply Hom.ext
[GOAL]
case hom
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
⊢ ((Hom.mk fun g => (g.fst, ↑X.ρ g.fst⁻¹ g.snd)) ≫ Hom.mk fun g => (g.fst, ↑X.ρ g.fst g.snd)).hom =
    (𝟙 (leftRegular G ⊗ X)).hom
[PROOFSTEP]
funext x
[GOAL]
case hom.h
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
x : (leftRegular G ⊗ X).V
⊢ Hom.hom ((Hom.mk fun g => (g.fst, ↑X.ρ g.fst⁻¹ g.snd)) ≫ Hom.mk fun g => (g.fst, ↑X.ρ g.fst g.snd)) x =
    Hom.hom (𝟙 (leftRegular G ⊗ X)) x
[PROOFSTEP]
refine' Prod.ext rfl _
[GOAL]
case hom.h
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
x : (leftRegular G ⊗ X).V
⊢ (Hom.hom ((Hom.mk fun g => (g.fst, ↑X.ρ g.fst⁻¹ g.snd)) ≫ Hom.mk fun g => (g.fst, ↑X.ρ g.fst g.snd)) x).snd =
    (Hom.hom (𝟙 (leftRegular G ⊗ X)) x).snd
[PROOFSTEP]
change (X.ρ x.1 * X.ρ (x.1⁻¹ : G)) x.2 = x.2
[GOAL]
case hom.h
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
x : (leftRegular G ⊗ X).V
⊢ (↑X.ρ x.fst * ↑X.ρ x.fst⁻¹) x.snd = x.snd
[PROOFSTEP]
rw [← X.ρ.map_mul, mul_inv_self, X.ρ.map_one, MonCat.one_of, End.one_def, types_id_apply]
[GOAL]
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
⊢ ((Hom.mk fun g => (g.fst, ↑X.ρ g.fst g.snd)) ≫ Hom.mk fun g => (g.fst, ↑X.ρ g.fst⁻¹ g.snd)) =
    𝟙 (leftRegular G ⊗ { V := X.V, ρ := 1 })
[PROOFSTEP]
apply Hom.ext
[GOAL]
case hom
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
⊢ ((Hom.mk fun g => (g.fst, ↑X.ρ g.fst g.snd)) ≫ Hom.mk fun g => (g.fst, ↑X.ρ g.fst⁻¹ g.snd)).hom =
    (𝟙 (leftRegular G ⊗ { V := X.V, ρ := 1 })).hom
[PROOFSTEP]
funext x
[GOAL]
case hom.h
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
x : (leftRegular G ⊗ { V := X.V, ρ := 1 }).V
⊢ Hom.hom ((Hom.mk fun g => (g.fst, ↑X.ρ g.fst g.snd)) ≫ Hom.mk fun g => (g.fst, ↑X.ρ g.fst⁻¹ g.snd)) x =
    Hom.hom (𝟙 (leftRegular G ⊗ { V := X.V, ρ := 1 })) x
[PROOFSTEP]
refine' Prod.ext rfl _
[GOAL]
case hom.h
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
x : (leftRegular G ⊗ { V := X.V, ρ := 1 }).V
⊢ (Hom.hom ((Hom.mk fun g => (g.fst, ↑X.ρ g.fst g.snd)) ≫ Hom.mk fun g => (g.fst, ↑X.ρ g.fst⁻¹ g.snd)) x).snd =
    (Hom.hom (𝟙 (leftRegular G ⊗ { V := X.V, ρ := 1 })) x).snd
[PROOFSTEP]
change (X.ρ (x.1⁻¹ : G) * X.ρ x.1) x.2 = x.2
[GOAL]
case hom.h
V : Type (u + 1)
inst✝² : LargeCategory V
G✝ H : MonCat
f : G✝ ⟶ H
R : Type u_1
inst✝¹ : Semiring R
G : Type u
inst✝ : Group G
X : Action (Type u) (MonCat.of G)
x : (leftRegular G ⊗ { V := X.V, ρ := 1 }).V
⊢ (↑X.ρ x.fst⁻¹ * ↑X.ρ x.fst) x.snd = x.snd
[PROOFSTEP]
rw [← X.ρ.map_mul, inv_mul_self, X.ρ.map_one, MonCat.one_of, End.one_def, types_id_apply]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
W : Type (u + 1)
inst✝ : LargeCategory W
F : V ⥤ W
G : MonCat
M : Action V G
⊢ (fun g => F.map (↑M.ρ g)) 1 = 1
[PROOFSTEP]
simp only [End.one_def, Action.ρ_one, F.map_id, MonCat.one_of]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
W : Type (u + 1)
inst✝ : LargeCategory W
F : V ⥤ W
G : MonCat
M : Action V G
g h : ↑G
⊢ OneHom.toFun { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) } (g * h) =
    OneHom.toFun { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) } g *
      OneHom.toFun { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) } h
[PROOFSTEP]
dsimp
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
W : Type (u + 1)
inst✝ : LargeCategory W
F : V ⥤ W
G : MonCat
M : Action V G
g h : ↑G
⊢ F.map (↑M.ρ (g * h)) = F.map (↑M.ρ g) * F.map (↑M.ρ h)
[PROOFSTEP]
rw [map_mul, MonCat.mul_of, End.mul_def, End.mul_def, F.map_comp]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
W : Type (u + 1)
inst✝ : LargeCategory W
F : V ⥤ W
G : MonCat
X✝ Y✝ : Action V G
f : X✝ ⟶ Y✝
g : ↑G
⊢ ↑((fun M =>
                { V := F.obj M.V,
                  ρ :=
                    {
                      toOneHom :=
                        { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) },
                      map_mul' :=
                        (_ :
                          ∀ (g h : ↑G),
                            OneHom.toFun
                                { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                (g * h) =
                              OneHom.toFun
                                  { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                  g *
                                OneHom.toFun
                                  { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                  h) } })
              X✝).ρ
        g ≫
      F.map f.hom =
    F.map f.hom ≫
      ↑((fun M =>
                { V := F.obj M.V,
                  ρ :=
                    {
                      toOneHom :=
                        { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) },
                      map_mul' :=
                        (_ :
                          ∀ (g h : ↑G),
                            OneHom.toFun
                                { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                (g * h) =
                              OneHom.toFun
                                  { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                  g *
                                OneHom.toFun
                                  { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                  h) } })
              Y✝).ρ
        g
[PROOFSTEP]
dsimp
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
W : Type (u + 1)
inst✝ : LargeCategory W
F : V ⥤ W
G : MonCat
X✝ Y✝ : Action V G
f : X✝ ⟶ Y✝
g : ↑G
⊢ F.map (↑X✝.ρ g) ≫ F.map f.hom = F.map f.hom ≫ F.map (↑Y✝.ρ g)
[PROOFSTEP]
rw [← F.map_comp, f.comm, F.map_comp]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
W : Type (u + 1)
inst✝ : LargeCategory W
F : V ⥤ W
G : MonCat
M : Action V G
⊢ {
          obj := fun M =>
            { V := F.obj M.V,
              ρ :=
                { toOneHom := { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) },
                  map_mul' :=
                    (_ :
                      ∀ (g h : ↑G),
                        OneHom.toFun
                            { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                            (g * h) =
                          OneHom.toFun
                              { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) } g *
                            OneHom.toFun
                              { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                              h) } },
          map := fun {X Y} f => Action.Hom.mk (F.map f.hom) }.map
      (𝟙 M) =
    𝟙
      ({
            obj := fun M =>
              { V := F.obj M.V,
                ρ :=
                  { toOneHom := { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) },
                    map_mul' :=
                      (_ :
                        ∀ (g h : ↑G),
                          OneHom.toFun
                              { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                              (g * h) =
                            OneHom.toFun
                                { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                g *
                              OneHom.toFun
                                { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                h) } },
            map := fun {X Y} f => Action.Hom.mk (F.map f.hom) }.obj
        M)
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝¹ : LargeCategory V
W : Type (u + 1)
inst✝ : LargeCategory W
F : V ⥤ W
G : MonCat
M : Action V G
⊢ ({
            obj := fun M =>
              { V := F.obj M.V,
                ρ :=
                  { toOneHom := { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) },
                    map_mul' :=
                      (_ :
                        ∀ (g h : ↑G),
                          OneHom.toFun
                              { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                              (g * h) =
                            OneHom.toFun
                                { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                g *
                              OneHom.toFun
                                { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                h) } },
            map := fun {X Y} f => Action.Hom.mk (F.map f.hom) }.map
        (𝟙 M)).hom =
    (𝟙
        ({
              obj := fun M =>
                { V := F.obj M.V,
                  ρ :=
                    {
                      toOneHom :=
                        { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) },
                      map_mul' :=
                        (_ :
                          ∀ (g h : ↑G),
                            OneHom.toFun
                                { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                (g * h) =
                              OneHom.toFun
                                  { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                  g *
                                OneHom.toFun
                                  { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                  h) } },
              map := fun {X Y} f => Action.Hom.mk (F.map f.hom) }.obj
          M)).hom
[PROOFSTEP]
simp only [Action.id_hom, F.map_id]
[GOAL]
V : Type (u + 1)
inst✝¹ : LargeCategory V
W : Type (u + 1)
inst✝ : LargeCategory W
F : V ⥤ W
G : MonCat
X✝ Y✝ Z✝ : Action V G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ {
          obj := fun M =>
            { V := F.obj M.V,
              ρ :=
                { toOneHom := { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) },
                  map_mul' :=
                    (_ :
                      ∀ (g h : ↑G),
                        OneHom.toFun
                            { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                            (g * h) =
                          OneHom.toFun
                              { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) } g *
                            OneHom.toFun
                              { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                              h) } },
          map := fun {X Y} f => Action.Hom.mk (F.map f.hom) }.map
      (f ≫ g) =
    {
            obj := fun M =>
              { V := F.obj M.V,
                ρ :=
                  { toOneHom := { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) },
                    map_mul' :=
                      (_ :
                        ∀ (g h : ↑G),
                          OneHom.toFun
                              { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                              (g * h) =
                            OneHom.toFun
                                { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                g *
                              OneHom.toFun
                                { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                h) } },
            map := fun {X Y} f => Action.Hom.mk (F.map f.hom) }.map
        f ≫
      {
            obj := fun M =>
              { V := F.obj M.V,
                ρ :=
                  { toOneHom := { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) },
                    map_mul' :=
                      (_ :
                        ∀ (g h : ↑G),
                          OneHom.toFun
                              { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                              (g * h) =
                            OneHom.toFun
                                { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                g *
                              OneHom.toFun
                                { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                h) } },
            map := fun {X Y} f => Action.Hom.mk (F.map f.hom) }.map
        g
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝¹ : LargeCategory V
W : Type (u + 1)
inst✝ : LargeCategory W
F : V ⥤ W
G : MonCat
X✝ Y✝ Z✝ : Action V G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ({
            obj := fun M =>
              { V := F.obj M.V,
                ρ :=
                  { toOneHom := { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) },
                    map_mul' :=
                      (_ :
                        ∀ (g h : ↑G),
                          OneHom.toFun
                              { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                              (g * h) =
                            OneHom.toFun
                                { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                g *
                              OneHom.toFun
                                { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                h) } },
            map := fun {X Y} f => Action.Hom.mk (F.map f.hom) }.map
        (f ≫ g)).hom =
    ({
              obj := fun M =>
                { V := F.obj M.V,
                  ρ :=
                    {
                      toOneHom :=
                        { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) },
                      map_mul' :=
                        (_ :
                          ∀ (g h : ↑G),
                            OneHom.toFun
                                { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                (g * h) =
                              OneHom.toFun
                                  { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                  g *
                                OneHom.toFun
                                  { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                  h) } },
              map := fun {X Y} f => Action.Hom.mk (F.map f.hom) }.map
          f ≫
        {
              obj := fun M =>
                { V := F.obj M.V,
                  ρ :=
                    {
                      toOneHom :=
                        { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) },
                      map_mul' :=
                        (_ :
                          ∀ (g h : ↑G),
                            OneHom.toFun
                                { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                (g * h) =
                              OneHom.toFun
                                  { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                  g *
                                OneHom.toFun
                                  { toFun := fun g => F.map (↑M.ρ g), map_one' := (_ : F.map (↑M.ρ 1) = 𝟙 (F.obj M.V)) }
                                  h) } },
              map := fun {X Y} f => Action.Hom.mk (F.map f.hom) }.map
          g).hom
[PROOFSTEP]
simp only [Action.comp_hom, F.map_comp]
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
g : ↑G
⊢ ↑(MonoidalCategory.tensorUnit (Action W G)).ρ g ≫ F.ε =
    F.ε ≫ ↑((Functor.mk src✝.toPrefunctor).obj (MonoidalCategory.tensorUnit (Action V G))).ρ g
[PROOFSTEP]
dsimp [FunctorCategoryEquivalence.inverse, Functor.mapAction]
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
g : ↑G
⊢ 𝟙 (MonoidalCategory.tensorUnit W) ≫ F.ε = F.ε ≫ F.map (𝟙 (MonoidalCategory.tensorUnit V))
[PROOFSTEP]
rw [Category.id_comp, F.map_id, Category.comp_id]
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
⊢ ∀ {X Y X' Y' : Action V G} (f : X ⟶ Y) (g : X' ⟶ Y'),
    MonoidalCategory.tensorHom ((Functor.mk src✝.toPrefunctor).map f) ((Functor.mk src✝.toPrefunctor).map g) ≫
        (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) Y Y' =
      (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) X X' ≫
        (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.tensorHom f g)
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
X✝ Y✝ X'✝ Y'✝ : Action V G
f✝ : X✝ ⟶ Y✝
g✝ : X'✝ ⟶ Y'✝
⊢ MonoidalCategory.tensorHom ((Functor.mk src✝.toPrefunctor).map f✝) ((Functor.mk src✝.toPrefunctor).map g✝) ≫
      (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) Y✝ Y'✝ =
    (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) X✝ X'✝ ≫
      (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.tensorHom f✝ g✝)
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
X✝ Y✝ X'✝ Y'✝ : Action V G
f✝ : X✝ ⟶ Y✝
g✝ : X'✝ ⟶ Y'✝
⊢ (MonoidalCategory.tensorHom ((Functor.mk src✝.toPrefunctor).map f✝) ((Functor.mk src✝.toPrefunctor).map g✝) ≫
        (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) Y✝ Y'✝).hom =
    ((fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) X✝ X'✝ ≫
        (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.tensorHom f✝ g✝)).hom
[PROOFSTEP]
simp
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
⊢ ∀ (X Y Z : Action V G),
    MonoidalCategory.tensorHom ((fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) X Y)
          (𝟙 ((Functor.mk src✝.toPrefunctor).obj Z)) ≫
        (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) (MonoidalCategory.tensorObj X Y) Z ≫
          (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.associator X Y Z).hom =
      (MonoidalCategory.associator ((Functor.mk src✝.toPrefunctor).obj X) ((Functor.mk src✝.toPrefunctor).obj Y)
            ((Functor.mk src✝.toPrefunctor).obj Z)).hom ≫
        MonoidalCategory.tensorHom (𝟙 ((Functor.mk src✝.toPrefunctor).obj X))
            ((fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) Y Z) ≫
          (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) X (MonoidalCategory.tensorObj Y Z)
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
X✝ Y✝ Z✝ : Action V G
⊢ MonoidalCategory.tensorHom ((fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) X✝ Y✝)
        (𝟙 ((Functor.mk src✝.toPrefunctor).obj Z✝)) ≫
      (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) (MonoidalCategory.tensorObj X✝ Y✝) Z✝ ≫
        (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.associator X✝ Y✝ Z✝).hom =
    (MonoidalCategory.associator ((Functor.mk src✝.toPrefunctor).obj X✝) ((Functor.mk src✝.toPrefunctor).obj Y✝)
          ((Functor.mk src✝.toPrefunctor).obj Z✝)).hom ≫
      MonoidalCategory.tensorHom (𝟙 ((Functor.mk src✝.toPrefunctor).obj X✝))
          ((fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) Y✝ Z✝) ≫
        (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) X✝ (MonoidalCategory.tensorObj Y✝ Z✝)
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
X✝ Y✝ Z✝ : Action V G
⊢ (MonoidalCategory.tensorHom ((fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) X✝ Y✝)
          (𝟙 ((Functor.mk src✝.toPrefunctor).obj Z✝)) ≫
        (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) (MonoidalCategory.tensorObj X✝ Y✝)
            Z✝ ≫
          (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.associator X✝ Y✝ Z✝).hom).hom =
    ((MonoidalCategory.associator ((Functor.mk src✝.toPrefunctor).obj X✝) ((Functor.mk src✝.toPrefunctor).obj Y✝)
            ((Functor.mk src✝.toPrefunctor).obj Z✝)).hom ≫
        MonoidalCategory.tensorHom (𝟙 ((Functor.mk src✝.toPrefunctor).obj X✝))
            ((fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) Y✝ Z✝) ≫
          (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) X✝
            (MonoidalCategory.tensorObj Y✝ Z✝)).hom
[PROOFSTEP]
simp
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
⊢ ∀ (X : Action V G),
    (MonoidalCategory.leftUnitor ((Functor.mk src✝.toPrefunctor).obj X)).hom =
      MonoidalCategory.tensorHom (Hom.mk F.ε) (𝟙 ((Functor.mk src✝.toPrefunctor).obj X)) ≫
        (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V))
            (MonoidalCategory.tensorUnit (Action V G)) X ≫
          (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.leftUnitor X).hom
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
X✝ : Action V G
⊢ (MonoidalCategory.leftUnitor ((Functor.mk src✝.toPrefunctor).obj X✝)).hom =
    MonoidalCategory.tensorHom (Hom.mk F.ε) (𝟙 ((Functor.mk src✝.toPrefunctor).obj X✝)) ≫
      (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V))
          (MonoidalCategory.tensorUnit (Action V G)) X✝ ≫
        (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.leftUnitor X✝).hom
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
X✝ : Action V G
⊢ (MonoidalCategory.leftUnitor ((Functor.mk src✝.toPrefunctor).obj X✝)).hom.hom =
    (MonoidalCategory.tensorHom (Hom.mk F.ε) (𝟙 ((Functor.mk src✝.toPrefunctor).obj X✝)) ≫
        (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V))
            (MonoidalCategory.tensorUnit (Action V G)) X✝ ≫
          (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.leftUnitor X✝).hom).hom
[PROOFSTEP]
simp
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
⊢ ∀ (X : Action V G),
    (MonoidalCategory.rightUnitor ((Functor.mk src✝.toPrefunctor).obj X)).hom =
      MonoidalCategory.tensorHom (𝟙 ((Functor.mk src✝.toPrefunctor).obj X)) (Hom.mk F.ε) ≫
        (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) X
            (MonoidalCategory.tensorUnit (Action V G)) ≫
          (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.rightUnitor X).hom
[PROOFSTEP]
intros
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
X✝ : Action V G
⊢ (MonoidalCategory.rightUnitor ((Functor.mk src✝.toPrefunctor).obj X✝)).hom =
    MonoidalCategory.tensorHom (𝟙 ((Functor.mk src✝.toPrefunctor).obj X✝)) (Hom.mk F.ε) ≫
      (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) X✝
          (MonoidalCategory.tensorUnit (Action V G)) ≫
        (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.rightUnitor X✝).hom
[PROOFSTEP]
ext
[GOAL]
case h
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
X✝ : Action V G
⊢ (MonoidalCategory.rightUnitor ((Functor.mk src✝.toPrefunctor).obj X✝)).hom.hom =
    (MonoidalCategory.tensorHom (𝟙 ((Functor.mk src✝.toPrefunctor).obj X✝)) (Hom.mk F.ε) ≫
        (fun X Y => Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)) X✝
            (MonoidalCategory.tensorUnit (Action V G)) ≫
          (Functor.mk src✝.toPrefunctor).map (MonoidalCategory.rightUnitor X✝).hom).hom
[PROOFSTEP]
dsimp
[GOAL]
case h
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
X✝ : Action V G
⊢ (MonoidalCategory.tensorHom (𝟙 (F.obj X✝.V)) (𝟙 (MonoidalCategory.tensorUnit W)) ≫
        (MonoidalCategory.rightUnitor (F.obj X✝.V)).hom) ≫
      𝟙 (F.obj X✝.V) =
    MonoidalCategory.tensorHom (𝟙 (F.obj X✝.V)) F.ε ≫
      LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X✝.V (MonoidalCategory.tensorUnit V) ≫
        F.map
          ((MonoidalCategory.tensorHom (𝟙 X✝.V) (𝟙 (MonoidalCategory.tensorUnit V)) ≫
              (MonoidalCategory.rightUnitor X✝.V).hom) ≫
            𝟙 X✝.V)
[PROOFSTEP]
simp only [MonoidalCategory.rightUnitor_conjugation, LaxMonoidalFunctor.right_unitality, Category.id_comp,
  Category.assoc, LaxMonoidalFunctor.right_unitality_inv_assoc, Category.comp_id, Iso.hom_inv_id]
[GOAL]
case h
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
X✝ : Action V G
⊢ MonoidalCategory.tensorHom (𝟙 (F.obj X✝.V)) F.ε ≫
      LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X✝.V (MonoidalCategory.tensorUnit V) ≫
        F.map (MonoidalCategory.rightUnitor X✝.V).hom ≫
          F.map (MonoidalCategory.rightUnitor X✝.V).inv ≫ F.map (MonoidalCategory.rightUnitor X✝.V).hom =
    MonoidalCategory.tensorHom (𝟙 (F.obj X✝.V)) F.ε ≫
      LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X✝.V (MonoidalCategory.tensorUnit V) ≫
        F.map (MonoidalCategory.rightUnitor X✝.V).hom
[PROOFSTEP]
rw [← F.map_comp, Iso.inv_hom_id, F.map_id, Category.comp_id]
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
⊢ IsIso
    (LaxMonoidalFunctor.mk (Functor.mk src✝.toPrefunctor) (Hom.mk F.ε) fun X Y =>
        Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)).ε
[PROOFSTEP]
infer_instance
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
src✝ : Action V G ⥤ Action W G := Functor.mapAction F.toFunctor G
⊢ ∀ (X Y : Action V G),
    IsIso
      (LaxMonoidalFunctor.μ
        (LaxMonoidalFunctor.mk (Functor.mk src✝.toPrefunctor) (Hom.mk F.ε) fun X Y =>
          Hom.mk (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V))
        X Y)
[PROOFSTEP]
infer_instance
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
⊢ (inv (mapAction F G).toLaxMonoidalFunctor.ε).hom = inv F.ε
[PROOFSTEP]
rw [← cancel_mono F.ε, IsIso.inv_hom_id, ← F.mapAction_toLaxMonoidalFunctor_ε_hom G, ← Action.comp_hom,
  IsIso.inv_hom_id, Action.id_hom]
[GOAL]
V : Type (u + 1)
inst✝³ : LargeCategory V
W : Type (u + 1)
inst✝² : LargeCategory W
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalCategory W
F : MonoidalFunctor V W
G : MonCat
X Y : Action V G
⊢ (inv (LaxMonoidalFunctor.μ (mapAction F G).toLaxMonoidalFunctor X Y)).hom =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X.V Y.V)
[PROOFSTEP]
rw [← cancel_mono (F.μ X.V Y.V), IsIso.inv_hom_id, ← F.mapAction_toLaxMonoidalFunctor_μ_hom G, ← Action.comp_hom,
  IsIso.inv_hom_id, Action.id_hom]
