/-
Copyright (c) 2022 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies

! This file was ported from Lean 3 source module group_theory.group_action.sigma
! leanprover-community/mathlib commit f1a2caaf51ef593799107fe9a8d5e411599f3996
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.GroupTheory.GroupAction.Defs

/-!
# Sigma instances for additive and multiplicative actions

This file defines instances for arbitrary sum of additive and multiplicative actions.

## See also

* `GroupTheory.GroupAction.Pi`
* `GroupTheory.GroupAction.Prod`
* `GroupTheory.GroupAction.Sum`
-/


variable {
ι: Type ?u.16
ι : 
Type _: Type (?u.2710+1)
Type _} {
M: Type ?u.5
M 
N: Type ?u.8
N : 
Type _: Type (?u.1445+1)
Type _} {
α: ι → Type ?u.13
α : 
ι: Type ?u.3996
ι → 
Type _: Type (?u.27+1)
Type _}

namespace Sigma

section SMul

variable [∀ 
i: ?m.31
i, 
SMul: Type ?u.734 → Type ?u.733 → Type (max?u.734?u.733)
SMul 
M: Type ?u.2713
M (
α: ι → Type ?u.2721
α 
i: ?m.1140
i)] [∀ 
i: ?m.2734
i, 
SMul: Type ?u.743 → Type ?u.742 → Type (max?u.743?u.742)
SMul 
N: Type ?u.22
N (
α: ι → Type ?u.1453
α 
i: ?m.40
i)] (
a: M
a : 
M: Type ?u.19
M) (
i: ι
i : 
ι: Type ?u.16
ι) (
b: α i
b : 
α: ι → Type ?u.1453
α 
i: ι
i) (
x: (i : ι) × α i
x : Σ
i: ?m.1484
i, 
α: ι → Type ?u.27
α 
i: ?m.58
i)

@[to_additive 
Sigma.VAdd: {ι : Type u_1} →
  {M : Type u_2} → {α : ι → Type u_3} → [inst : (i : ι) → _root_.VAdd M (α i)] → _root_.VAdd M ((i : ι) × α i)
Sigma.VAdd]
instance: {ι : Type u_1} → {M : Type u_2} → {α : ι → Type u_3} → [inst : (i : ι) → SMul M (α i)] → SMul M ((i : ι) × α i)
instance : 
SMul: Type ?u.113 → Type ?u.112 → Type (max?u.113?u.112)
SMul 
M: Type ?u.67
M (Σ
i: ?m.118
i, 
α: ι → Type ?u.75
α 
i: ?m.118
i) :=
  ⟨fun 
a: ?m.134
a => (
Sigma.map: {α₁ : Type ?u.139} →
  {α₂ : Type ?u.138} →
    {β₁ : α₁ → Type ?u.137} →
      {β₂ : α₂ → Type ?u.136} → (f₁ : α₁ → α₂) → ((a : α₁) → β₁ a → β₂ (f₁ a)) → Sigma β₁ → Sigma β₂
Sigma.map 
id: {α : Sort ?u.144} → α → α
id) fun 
_: ?m.161
_ => 
(· • ·): M → α x✝ → α (id x✝)
(· • ·) 
a: ?m.134
a⟩

@[
to_additive: ∀ {ι : Type u_1} {M : Type u_3} {α : ι → Type u_2} [inst : (i : ι) → _root_.VAdd M (α i)] (a : M) (x : (i : ι) × α i),
  a +ᵥ x = map id (fun x => (fun x_1 x_2 => x_1 +ᵥ x_2) a) x
to_additive]
theorem 
smul_def: a • x = map id (fun x => (fun x_1 x_2 => x_1 • x_2) a) x
smul_def : 
a: M
a • 
x: (i : ι) × α i
x = 
x: (i : ι) × α i
x.
map: {α₁ : Type ?u.853} →
  {α₂ : Type ?u.852} →
    {β₁ : α₁ → Type ?u.851} →
      {β₂ : α₂ → Type ?u.850} → (f₁ : α₁ → α₂) → ((a : α₁) → β₁ a → β₂ (f₁ a)) → Sigma β₁ → Sigma β₂
map 
id: {α : Sort ?u.865} → α → α
id fun 
_: ?m.871
_ => 
(· • ·): M → α x✝ → α (id x✝)
(· • ·) 
a: M
a :=
  
rfl: ∀ {α : Sort ?u.1041} {a : α}, a = a
rfl
#align sigma.smul_def 
Sigma.smul_def: ∀ {ι : Type u_1} {M : Type u_3} {α : ι → Type u_2} [inst : (i : ι) → SMul M (α i)] (a : M) (x : (i : ι) × α i),
  a • x = map id (fun x => (fun x_1 x_2 => x_1 • x_2) a) x
Sigma.smul_def
#align sigma.vadd_def 
Sigma.vadd_def: ∀ {ι : Type u_1} {M : Type u_3} {α : ι → Type u_2} [inst : (i : ι) → _root_.VAdd M (α i)] (a : M) (x : (i : ι) × α i),
  a +ᵥ x = map id (fun x => (fun x_1 x_2 => x_1 +ᵥ x_2) a) x
Sigma.vadd_def

@[
to_additive: ∀ {ι : Type u_1} {M : Type u_3} {α : ι → Type u_2} [inst : (i : ι) → _root_.VAdd M (α i)] (a : M) (i : ι) (b : α i),
  a +ᵥ { fst := i, snd := b } = { fst := i, snd := a +ᵥ b }
to_additive (attr := simp)]
theorem 
smul_mk: a • { fst := i, snd := b } = { fst := i, snd := a • b }
smul_mk : 
a: M
a • 
mk: {α : Type ?u.1183} → {β : α → Type ?u.1182} → (fst : α) → β fst → Sigma β
mk 
i: ι
i 
b: α i
b = ⟨
i: ι
i, 
a: M
a • 
b: α i
b⟩ :=
  
rfl: ∀ {α : Sort ?u.1314} {a : α}, a = a
rfl
#align sigma.smul_mk 
Sigma.smul_mk: ∀ {ι : Type u_1} {M : Type u_3} {α : ι → Type u_2} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι) (b : α i),
  a • { fst := i, snd := b } = { fst := i, snd := a • b }
Sigma.smul_mk
#align sigma.vadd_mk 
Sigma.vadd_mk: ∀ {ι : Type u_1} {M : Type u_3} {α : ι → Type u_2} [inst : (i : ι) → _root_.VAdd M (α i)] (a : M) (i : ι) (b : α i),
  a +ᵥ { fst := i, snd := b } = { fst := i, snd := a +ᵥ b }
Sigma.vadd_mk

@[
to_additive: ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → _root_.VAdd M (α i)]
  [inst_1 : (i : ι) → _root_.VAdd N (α i)] [inst_2 : _root_.VAdd M N] [inst_3 : ∀ (i : ι), VAddAssocClass M N (α i)],
  VAddAssocClass M N ((i : ι) × α i)
to_additive]
instance: ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)]
  [inst_1 : (i : ι) → SMul N (α i)] [inst_2 : SMul M N] [inst_3 : ∀ (i : ι), IsScalarTower M N (α i)],
  IsScalarTower M N ((i : ι) × α i)
instance [
SMul: Type ?u.1491 → Type ?u.1490 → Type (max?u.1491?u.1490)
SMul 
M: Type ?u.1445
M 
N: Type ?u.1448
N] [∀ 
i: ?m.1495
i, 
IsScalarTower: (M : Type ?u.1500) →
  (N : Type ?u.1499) → (α : Type ?u.1498) → [inst : SMul M N] → [inst : SMul N α] → [inst : SMul M α] → Prop
IsScalarTower 
M: Type ?u.1445
M 
N: Type ?u.1448
N (
α: ι → Type ?u.1453
α 
i: ?m.1495
i)] : 
IsScalarTower: (M : Type ?u.1549) →
  (N : Type ?u.1548) → (α : Type ?u.1547) → [inst : SMul M N] → [inst : SMul N α] → [inst : SMul M α] → Prop
IsScalarTower 
M: Type ?u.1445
M 
N: Type ?u.1448
N (Σ
i: ?m.1554
i, 
α: ι → Type ?u.1453
α 
i: ?m.1554
i) :=
  ⟨fun 
a: ?m.1757
a 
b: ?m.1760
b 
x: ?m.1763
x => by
Goals accomplished! 🐙
    
ι: Type ?u.1442

M: Type ?u.1445

N: Type ?u.1448

α: ι → Type ?u.1453

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x✝: (i : ι) × α i

inst✝¹: SMul M N

inst✝: ∀ (i : ι), IsScalarTower M N (α i)

a: M

b: N

x: (i : ι) × α i

(a • b) • x = a • b • xcases 
x: (i : ι) × α i
x
ι: Type ?u.1442

M: Type ?u.1445

N: Type ?u.1448

α: ι → Type ?u.1453

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝¹: SMul M N

inst✝: ∀ (i : ι), IsScalarTower M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
(a • b) • { fst := fst✝, snd := snd✝ } = a • b • { fst := fst✝, snd := snd✝ }
    
ι: Type ?u.1442

M: Type ?u.1445

N: Type ?u.1448

α: ι → Type ?u.1453

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x✝: (i : ι) × α i

inst✝¹: SMul M N

inst✝: ∀ (i : ι), IsScalarTower M N (α i)

a: M

b: N

x: (i : ι) × α i

(a • b) • x = a • b • xrw [
ι: Type ?u.1442

M: Type ?u.1445

N: Type ?u.1448

α: ι → Type ?u.1453

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝¹: SMul M N

inst✝: ∀ (i : ι), IsScalarTower M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
(a • b) • { fst := fst✝, snd := snd✝ } = a • b • { fst := fst✝, snd := snd✝ }
smul_mk: ∀ {ι : Type ?u.1936} {M : Type ?u.1938} {α : ι → Type ?u.1937} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι)
  (b : α i), a • { fst := i, snd := b } = { fst := i, snd := a • b }
smul_mk,
ι: Type ?u.1442

M: Type ?u.1445

N: Type ?u.1448

α: ι → Type ?u.1453

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝¹: SMul M N

inst✝: ∀ (i : ι), IsScalarTower M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
{ fst := fst✝, snd := (a • b) • snd✝ } = a • b • { fst := fst✝, snd := snd✝ } 
ι: Type ?u.1442

M: Type ?u.1445

N: Type ?u.1448

α: ι → Type ?u.1453

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝¹: SMul M N

inst✝: ∀ (i : ι), IsScalarTower M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
(a • b) • { fst := fst✝, snd := snd✝ } = a • b • { fst := fst✝, snd := snd✝ }
smul_mk: ∀ {ι : Type ?u.2061} {M : Type ?u.2063} {α : ι → Type ?u.2062} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι)
  (b : α i), a • { fst := i, snd := b } = { fst := i, snd := a • b }
smul_mk,
ι: Type ?u.1442

M: Type ?u.1445

N: Type ?u.1448

α: ι → Type ?u.1453

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝¹: SMul M N

inst✝: ∀ (i : ι), IsScalarTower M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
{ fst := fst✝, snd := (a • b) • snd✝ } =   { fst := (b • { fst := fst✝, snd := snd✝ }).fst, snd := a • (b • { fst := fst✝, snd := snd✝ }).snd } 
ι: Type ?u.1442

M: Type ?u.1445

N: Type ?u.1448

α: ι → Type ?u.1453

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝¹: SMul M N

inst✝: ∀ (i : ι), IsScalarTower M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
(a • b) • { fst := fst✝, snd := snd✝ } = a • b • { fst := fst✝, snd := snd✝ }
smul_mk: ∀ {ι : Type ?u.2185} {M : Type ?u.2187} {α : ι → Type ?u.2186} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι)
  (b : α i), a • { fst := i, snd := b } = { fst := i, snd := a • b }
smul_mk,
ι: Type ?u.1442

M: Type ?u.1445

N: Type ?u.1448

α: ι → Type ?u.1453

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝¹: SMul M N

inst✝: ∀ (i : ι), IsScalarTower M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
{ fst := fst✝, snd := (a • b) • snd✝ } =   { fst := { fst := fst✝, snd := b • snd✝ }.fst, snd := a • { fst := fst✝, snd := b • snd✝ }.snd } 
ι: Type ?u.1442

M: Type ?u.1445

N: Type ?u.1448

α: ι → Type ?u.1453

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝¹: SMul M N

inst✝: ∀ (i : ι), IsScalarTower M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
(a • b) • { fst := fst✝, snd := snd✝ } = a • b • { fst := fst✝, snd := snd✝ }
smul_assoc: ∀ {α : Type ?u.2274} {M : Type ?u.2272} {N : Type ?u.2273} [inst : SMul M N] [inst_1 : SMul N α] [inst_2 : SMul M α]
  [inst_3 : IsScalarTower M N α] (x : M) (y : N) (z : α), (x • y) • z = x • y • z
smul_assoc
ι: Type ?u.1442

M: Type ?u.1445

N: Type ?u.1448

α: ι → Type ?u.1453

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝¹: SMul M N

inst✝: ∀ (i : ι), IsScalarTower M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
{ fst := fst✝, snd := a • b • snd✝ } =   { fst := { fst := fst✝, snd := b • snd✝ }.fst, snd := a • { fst := fst✝, snd := b • snd✝ }.snd }]
Goals accomplished! 🐙⟩

@[
to_additive: ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → _root_.VAdd M (α i)]
  [inst_1 : (i : ι) → _root_.VAdd N (α i)] [inst_2 : ∀ (i : ι), VAddCommClass M N (α i)],
  VAddCommClass M N ((i : ι) × α i)
to_additive]
instance: ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)]
  [inst_1 : (i : ι) → SMul N (α i)] [inst_2 : ∀ (i : ι), SMulCommClass M N (α i)], SMulCommClass M N ((i : ι) × α i)
instance [∀ 
i: ?m.2759
i, 
SMulCommClass: (M : Type ?u.2764) → (N : Type ?u.2763) → (α : Type ?u.2762) → [inst : SMul M α] → [inst : SMul N α] → Prop
SMulCommClass 
M: Type ?u.2713
M 
N: Type ?u.2716
N (
α: ι → Type ?u.2721
α 
i: ?m.2759
i)] : 
SMulCommClass: (M : Type ?u.2800) → (N : Type ?u.2799) → (α : Type ?u.2798) → [inst : SMul M α] → [inst : SMul N α] → Prop
SMulCommClass 
M: Type ?u.2713
M 
N: Type ?u.2716
N (Σ
i: ?m.2805
i, 
α: ι → Type ?u.2721
α 
i: ?m.2805
i) :=
  ⟨fun 
a: ?m.2976
a 
b: ?m.2979
b 
x: ?m.2982
x => by
Goals accomplished! 🐙
    
ι: Type ?u.2710

M: Type ?u.2713

N: Type ?u.2716

α: ι → Type ?u.2721

inst✝²: (i : ι) → SMul M (α i)

inst✝¹: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x✝: (i : ι) × α i

inst✝: ∀ (i : ι), SMulCommClass M N (α i)

a: M

b: N

x: (i : ι) × α i

a • b • x = b • a • xcases 
x: (i : ι) × α i
x
ι: Type ?u.2710

M: Type ?u.2713

N: Type ?u.2716

α: ι → Type ?u.2721

inst✝²: (i : ι) → SMul M (α i)

inst✝¹: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝: ∀ (i : ι), SMulCommClass M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
a • b • { fst := fst✝, snd := snd✝ } = b • a • { fst := fst✝, snd := snd✝ }
    
ι: Type ?u.2710

M: Type ?u.2713

N: Type ?u.2716

α: ι → Type ?u.2721

inst✝²: (i : ι) → SMul M (α i)

inst✝¹: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x✝: (i : ι) × α i

inst✝: ∀ (i : ι), SMulCommClass M N (α i)

a: M

b: N

x: (i : ι) × α i

a • b • x = b • a • xrw [
ι: Type ?u.2710

M: Type ?u.2713

N: Type ?u.2716

α: ι → Type ?u.2721

inst✝²: (i : ι) → SMul M (α i)

inst✝¹: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝: ∀ (i : ι), SMulCommClass M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
a • b • { fst := fst✝, snd := snd✝ } = b • a • { fst := fst✝, snd := snd✝ }
smul_mk: ∀ {ι : Type ?u.3144} {M : Type ?u.3146} {α : ι → Type ?u.3145} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι)
  (b : α i), a • { fst := i, snd := b } = { fst := i, snd := a • b }
smul_mk,
ι: Type ?u.2710

M: Type ?u.2713

N: Type ?u.2716

α: ι → Type ?u.2721

inst✝²: (i : ι) → SMul M (α i)

inst✝¹: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝: ∀ (i : ι), SMulCommClass M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
{ fst := (b • { fst := fst✝, snd := snd✝ }).fst, snd := a • (b • { fst := fst✝, snd := snd✝ }).snd } =   b • a • { fst := fst✝, snd := snd✝ } 
ι: Type ?u.2710

M: Type ?u.2713

N: Type ?u.2716

α: ι → Type ?u.2721

inst✝²: (i : ι) → SMul M (α i)

inst✝¹: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝: ∀ (i : ι), SMulCommClass M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
a • b • { fst := fst✝, snd := snd✝ } = b • a • { fst := fst✝, snd := snd✝ }
smul_mk: ∀ {ι : Type ?u.3275} {M : Type ?u.3277} {α : ι → Type ?u.3276} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι)
  (b : α i), a • { fst := i, snd := b } = { fst := i, snd := a • b }
smul_mk,
ι: Type ?u.2710

M: Type ?u.2713

N: Type ?u.2716

α: ι → Type ?u.2721

inst✝²: (i : ι) → SMul M (α i)

inst✝¹: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝: ∀ (i : ι), SMulCommClass M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
{ fst := { fst := fst✝, snd := b • snd✝ }.fst, snd := a • { fst := fst✝, snd := b • snd✝ }.snd } =   b • a • { fst := fst✝, snd := snd✝ } 
ι: Type ?u.2710

M: Type ?u.2713

N: Type ?u.2716

α: ι → Type ?u.2721

inst✝²: (i : ι) → SMul M (α i)

inst✝¹: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝: ∀ (i : ι), SMulCommClass M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
a • b • { fst := fst✝, snd := snd✝ } = b • a • { fst := fst✝, snd := snd✝ }
smul_mk: ∀ {ι : Type ?u.3391} {M : Type ?u.3393} {α : ι → Type ?u.3392} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι)
  (b : α i), a • { fst := i, snd := b } = { fst := i, snd := a • b }
smul_mk,
ι: Type ?u.2710

M: Type ?u.2713

N: Type ?u.2716

α: ι → Type ?u.2721

inst✝²: (i : ι) → SMul M (α i)

inst✝¹: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝: ∀ (i : ι), SMulCommClass M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
{ fst := { fst := fst✝, snd := b • snd✝ }.fst, snd := a • { fst := fst✝, snd := b • snd✝ }.snd } =   { fst := (a • { fst := fst✝, snd := snd✝ }).fst, snd := b • (a • { fst := fst✝, snd := snd✝ }).snd } 
ι: Type ?u.2710

M: Type ?u.2713

N: Type ?u.2716

α: ι → Type ?u.2721

inst✝²: (i : ι) → SMul M (α i)

inst✝¹: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝: ∀ (i : ι), SMulCommClass M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
a • b • { fst := fst✝, snd := snd✝ } = b • a • { fst := fst✝, snd := snd✝ }
smul_mk: ∀ {ι : Type ?u.3489} {M : Type ?u.3491} {α : ι → Type ?u.3490} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι)
  (b : α i), a • { fst := i, snd := b } = { fst := i, snd := a • b }
smul_mk,
ι: Type ?u.2710

M: Type ?u.2713

N: Type ?u.2716

α: ι → Type ?u.2721

inst✝²: (i : ι) → SMul M (α i)

inst✝¹: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝: ∀ (i : ι), SMulCommClass M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
{ fst := { fst := fst✝, snd := b • snd✝ }.fst, snd := a • { fst := fst✝, snd := b • snd✝ }.snd } =   { fst := { fst := fst✝, snd := a • snd✝ }.fst, snd := b • { fst := fst✝, snd := a • snd✝ }.snd } 
ι: Type ?u.2710

M: Type ?u.2713

N: Type ?u.2716

α: ι → Type ?u.2721

inst✝²: (i : ι) → SMul M (α i)

inst✝¹: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝: ∀ (i : ι), SMulCommClass M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
a • b • { fst := fst✝, snd := snd✝ } = b • a • { fst := fst✝, snd := snd✝ }
smul_comm: ∀ {M : Type ?u.3580} {N : Type ?u.3579} {α : Type ?u.3578} [inst : SMul M α] [inst_1 : SMul N α]
  [self : SMulCommClass M N α] (m : M) (n : N) (a : α), m • n • a = n • m • a
smul_comm
ι: Type ?u.2710

M: Type ?u.2713

N: Type ?u.2716

α: ι → Type ?u.2721

inst✝²: (i : ι) → SMul M (α i)

inst✝¹: (i : ι) → SMul N (α i)

a✝: M

i: ι

b✝: α i

x: (i : ι) × α i

inst✝: ∀ (i : ι), SMulCommClass M N (α i)

a: M

b: N

fst✝: ι

snd✝: α fst✝

mk
{ fst := { fst := fst✝, snd := b • snd✝ }.fst, snd := b • a • snd✝ } =   { fst := { fst := fst✝, snd := a • snd✝ }.fst, snd := b • { fst := fst✝, snd := a • snd✝ }.snd }]
Goals accomplished! 🐙⟩

@[
to_additive: ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → _root_.VAdd M (α i)]
  [inst_1 : (i : ι) → _root_.VAdd Mᵃᵒᵖ (α i)] [inst_2 : ∀ (i : ι), IsCentralVAdd M (α i)],
  IsCentralVAdd M ((i : ι) × α i)
to_additive]
instance: ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → SMul M (α i)] [inst_1 : (i : ι) → SMul Mᵐᵒᵖ (α i)]
  [inst_2 : ∀ (i : ι), IsCentralScalar M (α i)], IsCentralScalar M ((i : ι) × α i)
instance [∀ 
i: ?m.4045
i, 
SMul: Type ?u.4049 → Type ?u.4048 → Type (max?u.4049?u.4048)
SMul 
M: Type ?u.3999
Mᵐᵒᵖ (
α: ι → Type ?u.4007
α 
i: ?m.4045
i)] [∀ 
i: ?m.4055
i, 
IsCentralScalar: (M : Type ?u.4059) → (α : Type ?u.4058) → [inst : SMul M α] → [inst : SMul Mᵐᵒᵖ α] → Prop
IsCentralScalar 
M: Type ?u.3999
M (
α: ι → Type ?u.4007
α 
i: ?m.4055
i)] : 
IsCentralScalar: (M : Type ?u.4093) → (α : Type ?u.4092) → [inst : SMul M α] → [inst : SMul Mᵐᵒᵖ α] → Prop
IsCentralScalar 
M: Type ?u.3999
M (Σ
i: ?m.4098
i, 
α: ι → Type ?u.4007
α 
i: ?m.4098
i) :=
  ⟨fun 
a: ?m.4263
a 
x: ?m.4266
x => by
Goals accomplished! 🐙
    
ι: Type ?u.3996

M: Type ?u.3999

N: Type ?u.4002

α: ι → Type ?u.4007

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b: α i

x✝: (i : ι) × α i

inst✝¹: (i : ι) → SMul Mᵐᵒᵖ (α i)

inst✝: ∀ (i : ι), IsCentralScalar M (α i)

a: M

x: (i : ι) × α i

MulOpposite.op a • x = a • xcases 
x: (i : ι) × α i
x
ι: Type ?u.3996

M: Type ?u.3999

N: Type ?u.4002

α: ι → Type ?u.4007

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b: α i

x: (i : ι) × α i

inst✝¹: (i : ι) → SMul Mᵐᵒᵖ (α i)

inst✝: ∀ (i : ι), IsCentralScalar M (α i)

a: M

fst✝: ι

snd✝: α fst✝

mk
MulOpposite.op a • { fst := fst✝, snd := snd✝ } = a • { fst := fst✝, snd := snd✝ }
    
ι: Type ?u.3996

M: Type ?u.3999

N: Type ?u.4002

α: ι → Type ?u.4007

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b: α i

x✝: (i : ι) × α i

inst✝¹: (i : ι) → SMul Mᵐᵒᵖ (α i)

inst✝: ∀ (i : ι), IsCentralScalar M (α i)

a: M

x: (i : ι) × α i

MulOpposite.op a • x = a • xrw [
ι: Type ?u.3996

M: Type ?u.3999

N: Type ?u.4002

α: ι → Type ?u.4007

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b: α i

x: (i : ι) × α i

inst✝¹: (i : ι) → SMul Mᵐᵒᵖ (α i)

inst✝: ∀ (i : ι), IsCentralScalar M (α i)

a: M

fst✝: ι

snd✝: α fst✝

mk
MulOpposite.op a • { fst := fst✝, snd := snd✝ } = a • { fst := fst✝, snd := snd✝ }
smul_mk: ∀ {ι : Type ?u.4430} {M : Type ?u.4432} {α : ι → Type ?u.4431} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι)
  (b : α i), a • { fst := i, snd := b } = { fst := i, snd := a • b }
smul_mk,
ι: Type ?u.3996

M: Type ?u.3999

N: Type ?u.4002

α: ι → Type ?u.4007

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b: α i

x: (i : ι) × α i

inst✝¹: (i : ι) → SMul Mᵐᵒᵖ (α i)

inst✝: ∀ (i : ι), IsCentralScalar M (α i)

a: M

fst✝: ι

snd✝: α fst✝

mk
{ fst := fst✝, snd := MulOpposite.op a • snd✝ } = a • { fst := fst✝, snd := snd✝ } 
ι: Type ?u.3996

M: Type ?u.3999

N: Type ?u.4002

α: ι → Type ?u.4007

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b: α i

x: (i : ι) × α i

inst✝¹: (i : ι) → SMul Mᵐᵒᵖ (α i)

inst✝: ∀ (i : ι), IsCentralScalar M (α i)

a: M

fst✝: ι

snd✝: α fst✝

mk
MulOpposite.op a • { fst := fst✝, snd := snd✝ } = a • { fst := fst✝, snd := snd✝ }
smul_mk: ∀ {ι : Type ?u.4551} {M : Type ?u.4553} {α : ι → Type ?u.4552} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι)
  (b : α i), a • { fst := i, snd := b } = { fst := i, snd := a • b }
smul_mk,
ι: Type ?u.3996

M: Type ?u.3999

N: Type ?u.4002

α: ι → Type ?u.4007

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b: α i

x: (i : ι) × α i

inst✝¹: (i : ι) → SMul Mᵐᵒᵖ (α i)

inst✝: ∀ (i : ι), IsCentralScalar M (α i)

a: M

fst✝: ι

snd✝: α fst✝

mk
{ fst := fst✝, snd := MulOpposite.op a • snd✝ } = { fst := fst✝, snd := a • snd✝ } 
ι: Type ?u.3996

M: Type ?u.3999

N: Type ?u.4002

α: ι → Type ?u.4007

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b: α i

x: (i : ι) × α i

inst✝¹: (i : ι) → SMul Mᵐᵒᵖ (α i)

inst✝: ∀ (i : ι), IsCentralScalar M (α i)

a: M

fst✝: ι

snd✝: α fst✝

mk
MulOpposite.op a • { fst := fst✝, snd := snd✝ } = a • { fst := fst✝, snd := snd✝ }
op_smul_eq_smul: ∀ {M : Type ?u.4661} {α : Type ?u.4660} [inst : SMul M α] [inst_1 : SMul Mᵐᵒᵖ α] [self : IsCentralScalar M α] (m : M)
  (a : α), MulOpposite.op m • a = m • a
op_smul_eq_smul
ι: Type ?u.3996

M: Type ?u.3999

N: Type ?u.4002

α: ι → Type ?u.4007

inst✝³: (i : ι) → SMul M (α i)

inst✝²: (i : ι) → SMul N (α i)

a✝: M

i: ι

b: α i

x: (i : ι) × α i

inst✝¹: (i : ι) → SMul Mᵐᵒᵖ (α i)

inst✝: ∀ (i : ι), IsCentralScalar M (α i)

a: M

fst✝: ι

snd✝: α fst✝

mk
{ fst := fst✝, snd := a • snd✝ } = { fst := fst✝, snd := a • snd✝ }]
Goals accomplished! 🐙⟩

/-- This is not an instance because `i` becomes a metavariable. -/
@[
to_additive: ∀ {ι : Type u_3} {M : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → _root_.VAdd M (α i)] (i : ι)
  [inst_1 : FaithfulVAdd M (α i)], FaithfulVAdd M ((i : ι) × α i)
to_additive "This is not an instance because `i` becomes a metavariable."]
protected theorem 
FaithfulSMul': ∀ {ι : Type u_3} {M : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → SMul M (α i)] (i : ι)
  [inst_1 : FaithfulSMul M (α i)], FaithfulSMul M ((i : ι) × α i)
FaithfulSMul' [
FaithfulSMul: (M : Type ?u.5029) → (α : Type ?u.5028) → [inst : SMul M α] → Prop
FaithfulSMul 
M: Type ?u.4983
M (
α: ι → Type ?u.4991
α 
i: ι
i)] : 
FaithfulSMul: (M : Type ?u.5049) → (α : Type ?u.5048) → [inst : SMul M α] → Prop
FaithfulSMul 
M: Type ?u.4983
M (Σ
i: ?m.5054
i, 
α: ι → Type ?u.4991
α 
i: ?m.5054
i) :=
  ⟨fun 
h: ?m.5150
h => 
eq_of_smul_eq_smul: ∀ {M : Type ?u.5154} {α : Type ?u.5153} [inst : SMul M α] [self : FaithfulSMul M α] {m₁ m₂ : M},
  (∀ (a : α), m₁ • a = m₂ • a) → m₁ = m₂
eq_of_smul_eq_smul fun 
a: α i
a : 
α: ι → Type ?u.4991
α 
i: ι
i => 
heq_iff_eq: ∀ {α : Sort ?u.5192} {a b : α}, HEq a b ↔ a = b
heq_iff_eq.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 (
ext_iff: ∀ {α : Type ?u.5203} {β : α → Type ?u.5204} {x₀ x₁ : Sigma β}, x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ HEq x₀.snd x₁.snd
ext_iff.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 <| 
h: ?m.5150
h <| 
mk: {α : Type ?u.5212} → {β : α → Type ?u.5211} → (fst : α) → β fst → Sigma β
mk 
i: ι
i 
a: α i
a).
2: ∀ {a b : Prop}, a ∧ b → b
2⟩
#align sigma.has_faithful_smul' 
Sigma.FaithfulSMul': ∀ {ι : Type u_3} {M : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → SMul M (α i)] (i : ι)
  [inst_1 : FaithfulSMul M (α i)], FaithfulSMul M ((i : ι) × α i)
Sigma.FaithfulSMul'
#align sigma.has_faithful_vadd' 
Sigma.FaithfulVAdd': ∀ {ι : Type u_3} {M : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → _root_.VAdd M (α i)] (i : ι)
  [inst_1 : FaithfulVAdd M (α i)], FaithfulVAdd M ((i : ι) × α i)
Sigma.FaithfulVAdd'

@[
to_additive: ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → _root_.VAdd M (α i)] [inst_1 : Nonempty ι]
  [inst_2 : ∀ (i : ι), FaithfulVAdd M (α i)], FaithfulVAdd M ((i : ι) × α i)
to_additive]
instance: ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → SMul M (α i)] [inst_1 : Nonempty ι]
  [inst_2 : ∀ (i : ι), FaithfulSMul M (α i)], FaithfulSMul M ((i : ι) × α i)
instance [
Nonempty: Sort ?u.5449 → Prop
Nonempty 
ι: Type ?u.5401
ι] [∀ 
i: ?m.5453
i, 
FaithfulSMul: (M : Type ?u.5457) → (α : Type ?u.5456) → [inst : SMul M α] → Prop
FaithfulSMul 
M: Type ?u.5404
M (
α: ι → Type ?u.5412
α 
i: ?m.5453
i)] : 
FaithfulSMul: (M : Type ?u.5478) → (α : Type ?u.5477) → [inst : SMul M α] → Prop
FaithfulSMul 
M: Type ?u.5404
M (Σ
i: ?m.5483
i, 
α: ι → Type ?u.5412
α 
i: ?m.5483
i) :=
  (
Nonempty.elim: ∀ {α : Sort ?u.5544} {p : Prop}, Nonempty α → (α → p) → p
Nonempty.elim ‹_›) fun 
i: ?m.5552
i => 
Sigma.FaithfulSMul': ∀ {ι : Type ?u.5556} {M : Type ?u.5554} {α : ι → Type ?u.5555} [inst : (i : ι) → SMul M (α i)] (i : ι)
  [inst_1 : FaithfulSMul M (α i)], FaithfulSMul M ((i : ι) × α i)
Sigma.FaithfulSMul' 
i: ?m.5552
i

end SMul

@[
to_additive: {ι : Type u_1} →
  {M : Type u_2} →
    {α : ι → Type u_3} → {m : AddMonoid M} → [inst : (i : ι) → AddAction M (α i)] → AddAction M ((i : ι) × α i)
to_additive]
instance: {ι : Type u_1} →
  {M : Type u_2} →
    {α : ι → Type u_3} → {m : Monoid M} → [inst : (i : ι) → MulAction M (α i)] → MulAction M ((i : ι) × α i)
instance {
m: Monoid M
m : 
Monoid: Type ?u.5790 → Type ?u.5790
Monoid 
M: Type ?u.5779
M} [∀ 
i: ?m.5794
i, 
MulAction: (α : Type ?u.5798) → Type ?u.5797 → [inst : Monoid α] → Type (max?u.5798?u.5797)
MulAction 
M: Type ?u.5779
M (
α: ι → Type ?u.5787
α 
i: ?m.5794
i)] :
    
MulAction: (α : Type ?u.5812) → Type ?u.5811 → [inst : Monoid α] → Type (max?u.5812?u.5811)
MulAction 
M: Type ?u.5779
M (Σ
i: ?m.5817
i, 
α: ι → Type ?u.5787
α 
i: ?m.5817
i) where
  mul_smul 
a: ?m.6449
a 
b: ?m.6452
b 
x: ?m.6455
x := by
Goals accomplished! 🐙
    
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

a, b: M

x: (i : ι) × α i

(a * b) • x = a • b • xcases 
x: (i : ι) × α i
x
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

a, b: M

fst✝: ι

snd✝: α fst✝

mk
(a * b) • { fst := fst✝, snd := snd✝ } = a • b • { fst := fst✝, snd := snd✝ }
    
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

a, b: M

x: (i : ι) × α i

(a * b) • x = a • b • xrw [
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

a, b: M

fst✝: ι

snd✝: α fst✝

mk
(a * b) • { fst := fst✝, snd := snd✝ } = a • b • { fst := fst✝, snd := snd✝ }
smul_mk: ∀ {ι : Type ?u.7224} {M : Type ?u.7226} {α : ι → Type ?u.7225} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι)
  (b : α i), a • { fst := i, snd := b } = { fst := i, snd := a • b }
smul_mk,
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

a, b: M

fst✝: ι

snd✝: α fst✝

mk
{ fst := fst✝, snd := (a * b) • snd✝ } = a • b • { fst := fst✝, snd := snd✝ } 
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

a, b: M

fst✝: ι

snd✝: α fst✝

mk
(a * b) • { fst := fst✝, snd := snd✝ } = a • b • { fst := fst✝, snd := snd✝ }
smul_mk: ∀ {ι : Type ?u.7297} {M : Type ?u.7299} {α : ι → Type ?u.7298} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι)
  (b : α i), a • { fst := i, snd := b } = { fst := i, snd := a • b }
smul_mk,
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

a, b: M

fst✝: ι

snd✝: α fst✝

mk
{ fst := fst✝, snd := (a * b) • snd✝ } =   { fst := (b • { fst := fst✝, snd := snd✝ }).fst, snd := a • (b • { fst := fst✝, snd := snd✝ }).snd } 
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

a, b: M

fst✝: ι

snd✝: α fst✝

mk
(a * b) • { fst := fst✝, snd := snd✝ } = a • b • { fst := fst✝, snd := snd✝ }
smul_mk: ∀ {ι : Type ?u.7379} {M : Type ?u.7381} {α : ι → Type ?u.7380} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι)
  (b : α i), a • { fst := i, snd := b } = { fst := i, snd := a • b }
smul_mk,
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

a, b: M

fst✝: ι

snd✝: α fst✝

mk
{ fst := fst✝, snd := (a * b) • snd✝ } =   { fst := { fst := fst✝, snd := b • snd✝ }.fst, snd := a • { fst := fst✝, snd := b • snd✝ }.snd } 
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

a, b: M

fst✝: ι

snd✝: α fst✝

mk
(a * b) • { fst := fst✝, snd := snd✝ } = a • b • { fst := fst✝, snd := snd✝ }
mul_smul: ∀ {α : Type ?u.7461} {β : Type ?u.7460} [inst : Monoid α] [self : MulAction α β] (x y : α) (b : β),
  (x * y) • b = x • y • b
mul_smul
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

a, b: M

fst✝: ι

snd✝: α fst✝

mk
{ fst := fst✝, snd := a • b • snd✝ } =   { fst := { fst := fst✝, snd := b • snd✝ }.fst, snd := a • { fst := fst✝, snd := b • snd✝ }.snd }]
Goals accomplished! 🐙
  one_smul 
x: ?m.6439
x := by
Goals accomplished! 🐙
    
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

x: (i : ι) × α i

1 • x = xcases 
x: (i : ι) × α i
x
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

fst✝: ι

snd✝: α fst✝

mk
1 • { fst := fst✝, snd := snd✝ } = { fst := fst✝, snd := snd✝ }
    
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

x: (i : ι) × α i

1 • x = xrw [
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

fst✝: ι

snd✝: α fst✝

mk
1 • { fst := fst✝, snd := snd✝ } = { fst := fst✝, snd := snd✝ }
smul_mk: ∀ {ι : Type ?u.6527} {M : Type ?u.6529} {α : ι → Type ?u.6528} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι)
  (b : α i), a • { fst := i, snd := b } = { fst := i, snd := a • b }
smul_mk,
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

fst✝: ι

snd✝: α fst✝

mk
{ fst := fst✝, snd := 1 • snd✝ } = { fst := fst✝, snd := snd✝ } 
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

fst✝: ι

snd✝: α fst✝

mk
1 • { fst := fst✝, snd := snd✝ } = { fst := fst✝, snd := snd✝ }
one_smul: ∀ (M : Type ?u.7127) {α : Type ?u.7126} [inst : Monoid M] [inst_1 : MulAction M α] (b : α), 1 • b = b
one_smul
ι: Type ?u.5776

M: Type ?u.5779

N: Type ?u.5782

α: ι → Type ?u.5787

m: Monoid M

inst✝: (i : ι) → MulAction M (α i)

fst✝: ι

snd✝: α fst✝

mk
{ fst := fst✝, snd := snd✝ } = { fst := fst✝, snd := snd✝ }]
Goals accomplished! 🐙

end Sigma