/-
Copyright (c) 2018 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, Patrick Massot

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

/-!
# Pi instances for multiplicative actions

This file defines instances for `MulAction` and related structures on `Pi` types.

## See also

* `GroupTheory.GroupAction.option`
* `GroupTheory.GroupAction.prod`
* `GroupTheory.GroupAction.sigma`
* `GroupTheory.GroupAction.sum`
-/


universe u v w

variable {I: Type u
I : Type u: Type (u+1)
Type u}

-- The indexing type
variable {f: I → Type v
f : I: Type u
I → Type v: Type (v+1)
Type v}

-- The family of types already equipped with instances
variable (x: (i : I) → f i
x y: (i : I) → f i
y : ∀ i: ?m.23
i, f: I → Type v
f i: ?m.17
i) (i: I
i : I: Type u
I)

namespace Pi

@[to_additive: {I : Type u} →
  {f : I → Type v} → {g : I → Type u_1} → [inst : (i : I) → VAdd (f i) (g i)] → VAdd ((i : I) → f i) ((i : I) → g i)
to_additive]
instance smul': {I : Type u} →
  {f : I → Type v} → {g : I → Type u_1} → [inst : (i : I) → SMul (f i) (g i)] → SMul ((i : I) → f i) ((i : I) → g i)
smul' {g: I → Type ?u.52
g : I: Type u
I → Type _: Type (?u.52+1)
Type _} [∀ i: ?m.56
i, SMul: Type ?u.60 → Type ?u.59 → Type (max?u.60?u.59)
SMul (f: I → Type v
f i: ?m.56
i) (g: I → Type ?u.52
g i: ?m.56
i)] : SMul: Type ?u.65 → Type ?u.64 → Type (max?u.65?u.64)
SMul (∀ i: ?m.67
i, f: I → Type v
f i: ?m.67
i) (∀ i: I
i : I: Type u
I, g: I → Type ?u.52
g i: I
i) :=
  ⟨fun s: ?m.91
s x: ?m.94
x => fun i: ?m.98
i => s: ?m.91
s i: ?m.98
i • x: ?m.94
x i: ?m.98
i⟩
#align pi.has_smul' Pi.smul': {I : Type u} →
  {f : I → Type v} → {g : I → Type u_1} → [inst : (i : I) → SMul (f i) (g i)] → SMul ((i : I) → f i) ((i : I) → g i)
Pi.smul'
#align pi.has_vadd' Pi.vadd': {I : Type u} →
  {f : I → Type v} → {g : I → Type u_1} → [inst : (i : I) → VAdd (f i) (g i)] → VAdd ((i : I) → f i) ((i : I) → g i)
Pi.vadd'

@[to_additive: ∀ {I : Type u} {f : I → Type v} (i : I) {g : I → Type u_1} [inst : (i : I) → VAdd (f i) (g i)] (s : (i : I) → f i)
  (x : (i : I) → g i), (s +ᵥ x) i = s i +ᵥ x i
to_additive (attr := simp)]
theorem smul_apply': ∀ {g : I → Type u_1} [inst : (i : I) → SMul (f i) (g i)] (s : (i : I) → f i) (x : (i : I) → g i), (s • x) i = s i • x i
smul_apply' {g: I → Type ?u.477
g : I: Type u
I → Type _: Type (?u.477+1)
Type _} [∀ i: ?m.481
i, SMul: Type ?u.485 → Type ?u.484 → Type (max?u.485?u.484)
SMul (f: I → Type v
f i: ?m.481
i) (g: I → Type ?u.477
g i: ?m.481
i)] (s: (i : I) → f i
s : ∀ i: ?m.490
i, f: I → Type v
f i: ?m.490
i) (x: (i : I) → g i
x : ∀ i: ?m.496
i, g: I → Type ?u.477
g i: ?m.496
i) :
    (s: (i : I) → f i
s • x: (i : I) → g i
x) i: I
i = s: (i : I) → f i
s i: I
i • x: (i : I) → g i
x i: I
i :=
  rfl: ∀ {α : Sort ?u.629} {a : α}, a = a
rfl
#align pi.smul_apply' Pi.smul_apply': ∀ {I : Type u} {f : I → Type v} (i : I) {g : I → Type u_1} [inst : (i : I) → SMul (f i) (g i)] (s : (i : I) → f i)
  (x : (i : I) → g i), (s • x) i = s i • x i
Pi.smul_apply'
#align pi.vadd_apply' Pi.vadd_apply': ∀ {I : Type u} {f : I → Type v} (i : I) {g : I → Type u_1} [inst : (i : I) → VAdd (f i) (g i)] (s : (i : I) → f i)
  (x : (i : I) → g i), (s +ᵥ x) i = s i +ᵥ x i
Pi.vadd_apply'

-- Porting note: `to_additive` fails to correctly translate name
@[to_additive Pi.vaddAssocClass: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [inst : VAdd α β] [inst_1 : (i : I) → VAdd β (f i)]
  [inst_2 : (i : I) → VAdd α (f i)] [inst_3 : ∀ (i : I), VAddAssocClass α β (f i)], VAddAssocClass α β ((i : I) → f i)
Pi.vaddAssocClass]
instance isScalarTower: ∀ {α : Type ?u.765} {β : Type ?u.768} [inst : SMul α β] [inst_1 : (i : I) → SMul β (f i)]
  [inst_2 : (i : I) → SMul α (f i)] [inst_3 : ∀ (i : I), IsScalarTower α β (f i)], IsScalarTower α β ((i : I) → f i)
isScalarTower {α: Type ?u.765
α β: Type ?u.768
β : Type _: Type (?u.768+1)
Type _} [SMul: Type ?u.772 → Type ?u.771 → Type (max?u.772?u.771)
SMul α: Type ?u.765
α β: Type ?u.768
β] [∀ i: ?m.776
i, SMul: Type ?u.780 → Type ?u.779 → Type (max?u.780?u.779)
SMul β: Type ?u.768
β <| f: I → Type v
f i: ?m.776
i]
    [∀ i: ?m.785
i, SMul: Type ?u.789 → Type ?u.788 → Type (max?u.789?u.788)
SMul α: Type ?u.765
α <| f: I → Type v
f i: ?m.785
i] [∀ i: ?m.794
i, IsScalarTower: (M : Type ?u.799) →
  (N : Type ?u.798) → (α : Type ?u.797) → [inst : SMul M N] → [inst : SMul N α] → [inst : SMul M α] → Prop
IsScalarTower α: Type ?u.765
α β: Type ?u.768
β (f: I → Type v
f i: ?m.794
i)] : IsScalarTower: (M : Type ?u.850) →
  (N : Type ?u.849) → (α : Type ?u.848) → [inst : SMul M N] → [inst : SMul N α] → [inst : SMul M α] → Prop
IsScalarTower α: Type ?u.765
α β: Type ?u.768
β (∀ i: I
i : I: Type u
I, f: I → Type v
f i: I
i) :=
  ⟨fun x: ?m.1060
x y: ?m.1063
y z: ?m.1066
z => funext: ∀ {α : Sort ?u.1069} {β : α → Sort ?u.1068} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun i: ?m.1083
i => smul_assoc: ∀ {α : Type ?u.1087} {M : Type ?u.1085} {N : Type ?u.1086} [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 x: ?m.1060
x y: ?m.1063
y (z: ?m.1066
z i: ?m.1083
i)⟩
#align pi.is_scalar_tower Pi.isScalarTower: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : (i : I) → SMul β (f i)]
  [inst_2 : (i : I) → SMul α (f i)] [inst_3 : ∀ (i : I), IsScalarTower α β (f i)], IsScalarTower α β ((i : I) → f i)
Pi.isScalarTower
#align pi.vadd_assoc_class Pi.vaddAssocClass: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [inst : VAdd α β] [inst_1 : (i : I) → VAdd β (f i)]
  [inst_2 : (i : I) → VAdd α (f i)] [inst_3 : ∀ (i : I), VAddAssocClass α β (f i)], VAddAssocClass α β ((i : I) → f i)
Pi.vaddAssocClass

@[to_additive Pi.vaddAssocClass': ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [inst : (i : I) → VAdd α (f i)]
  [inst_1 : (i : I) → VAdd (f i) (g i)] [inst_2 : (i : I) → VAdd α (g i)]
  [inst_3 : ∀ (i : I), VAddAssocClass α (f i) (g i)], VAddAssocClass α ((i : I) → f i) ((i : I) → g i)
Pi.vaddAssocClass']
instance isScalarTower': ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [inst : (i : I) → SMul α (f i)]
  [inst_1 : (i : I) → SMul (f i) (g i)] [inst_2 : (i : I) → SMul α (g i)]
  [inst_3 : ∀ (i : I), IsScalarTower α (f i) (g i)], IsScalarTower α ((i : I) → f i) ((i : I) → g i)
isScalarTower' {g: I → Type ?u.1475
g : I: Type u
I → Type _: Type (?u.1475+1)
Type _} {α: Type ?u.1478
α : Type _: Type (?u.1478+1)
Type _} [∀ i: ?m.1482
i, SMul: Type ?u.1486 → Type ?u.1485 → Type (max?u.1486?u.1485)
SMul α: Type ?u.1478
α <| f: I → Type v
f i: ?m.1482
i]
    [∀ i: ?m.1491
i, SMul: Type ?u.1495 → Type ?u.1494 → Type (max?u.1495?u.1494)
SMul (f: I → Type v
f i: ?m.1491
i) (g: I → Type ?u.1475
g i: ?m.1491
i)] [∀ i: ?m.1500
i, SMul: Type ?u.1504 → Type ?u.1503 → Type (max?u.1504?u.1503)
SMul α: Type ?u.1478
α <| g: I → Type ?u.1475
g i: ?m.1500
i] [∀ i: ?m.1509
i, IsScalarTower: (M : Type ?u.1514) →
  (N : Type ?u.1513) → (α : Type ?u.1512) → [inst : SMul M N] → [inst : SMul N α] → [inst : SMul M α] → Prop
IsScalarTower α: Type ?u.1478
α (f: I → Type v
f i: ?m.1509
i) (g: I → Type ?u.1475
g i: ?m.1509
i)] :
    IsScalarTower: (M : Type ?u.1570) →
  (N : Type ?u.1569) → (α : Type ?u.1568) → [inst : SMul M N] → [inst : SMul N α] → [inst : SMul M α] → Prop
IsScalarTower α: Type ?u.1478
α (∀ i: I
i : I: Type u
I, f: I → Type v
f i: I
i) (∀ i: I
i : I: Type u
I, g: I → Type ?u.1475
g i: I
i) :=
  ⟨fun x: ?m.1848
x y: ?m.1851
y z: ?m.1854
z => funext: ∀ {α : Sort ?u.1858} {β : α → Sort ?u.1857} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun i: ?m.1872
i => smul_assoc: ∀ {α : Type ?u.1876} {M : Type ?u.1874} {N : Type ?u.1875} [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 x: ?m.1848
x (y: ?m.1851
y i: ?m.1872
i) (z: ?m.1854
z i: ?m.1872
i)⟩
#align pi.is_scalar_tower' Pi.isScalarTower': ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [inst : (i : I) → SMul α (f i)]
  [inst_1 : (i : I) → SMul (f i) (g i)] [inst_2 : (i : I) → SMul α (g i)]
  [inst_3 : ∀ (i : I), IsScalarTower α (f i) (g i)], IsScalarTower α ((i : I) → f i) ((i : I) → g i)
Pi.isScalarTower'
#align pi.vadd_assoc_class' Pi.vaddAssocClass': ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [inst : (i : I) → VAdd α (f i)]
  [inst_1 : (i : I) → VAdd (f i) (g i)] [inst_2 : (i : I) → VAdd α (g i)]
  [inst_3 : ∀ (i : I), VAddAssocClass α (f i) (g i)], VAddAssocClass α ((i : I) → f i) ((i : I) → g i)
Pi.vaddAssocClass'

@[to_additive Pi.vaddAssocClass'': ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [inst : (i : I) → VAdd (f i) (g i)]
  [inst_1 : (i : I) → VAdd (g i) (h i)] [inst_2 : (i : I) → VAdd (f i) (h i)]
  [inst_3 : ∀ (i : I), VAddAssocClass (f i) (g i) (h i)], VAddAssocClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
Pi.vaddAssocClass'']
instance isScalarTower'': ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [inst : (i : I) → SMul (f i) (g i)]
  [inst_1 : (i : I) → SMul (g i) (h i)] [inst_2 : (i : I) → SMul (f i) (h i)]
  [inst_3 : ∀ (i : I), IsScalarTower (f i) (g i) (h i)], IsScalarTower ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
isScalarTower'' {g: I → Type ?u.2363
g : I: Type u
I → Type _: Type (?u.2363+1)
Type _} {h: I → Type ?u.2368
h : I: Type u
I → Type _: Type (?u.2368+1)
Type _} [∀ i: ?m.2372
i, SMul: Type ?u.2376 → Type ?u.2375 → Type (max?u.2376?u.2375)
SMul (f: I → Type v
f i: ?m.2372
i) (g: I → Type ?u.2363
g i: ?m.2372
i)]
    [∀ i: ?m.2381
i, SMul: Type ?u.2385 → Type ?u.2384 → Type (max?u.2385?u.2384)
SMul (g: I → Type ?u.2363
g i: ?m.2381
i) (h: I → Type ?u.2368
h i: ?m.2381
i)] [∀ i: ?m.2390
i, SMul: Type ?u.2394 → Type ?u.2393 → Type (max?u.2394?u.2393)
SMul (f: I → Type v
f i: ?m.2390
i) (h: I → Type ?u.2368
h i: ?m.2390
i)] [∀ i: ?m.2399
i, IsScalarTower: (M : Type ?u.2404) →
  (N : Type ?u.2403) → (α : Type ?u.2402) → [inst : SMul M N] → [inst : SMul N α] → [inst : SMul M α] → Prop
IsScalarTower (f: I → Type v
f i: ?m.2399
i) (g: I → Type ?u.2363
g i: ?m.2399
i) (h: I → Type ?u.2368
h i: ?m.2399
i)] :
    IsScalarTower: (M : Type ?u.2461) →
  (N : Type ?u.2460) → (α : Type ?u.2459) → [inst : SMul M N] → [inst : SMul N α] → [inst : SMul M α] → Prop
IsScalarTower (∀ i: ?m.2463
i, f: I → Type v
f i: ?m.2463
i) (∀ i: ?m.2468
i, g: I → Type ?u.2363
g i: ?m.2468
i) (∀ i: ?m.2473
i, h: I → Type ?u.2368
h i: ?m.2473
i) :=
  ⟨fun x: ?m.2765
x y: ?m.2768
y z: ?m.2772
z => funext: ∀ {α : Sort ?u.2776} {β : α → Sort ?u.2775} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun i: ?m.2790
i => smul_assoc: ∀ {α : Type ?u.2794} {M : Type ?u.2792} {N : Type ?u.2793} [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 (x: ?m.2765
x i: ?m.2790
i) (y: ?m.2768
y i: ?m.2790
i) (z: ?m.2772
z i: ?m.2790
i)⟩
#align pi.is_scalar_tower'' Pi.isScalarTower'': ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [inst : (i : I) → SMul (f i) (g i)]
  [inst_1 : (i : I) → SMul (g i) (h i)] [inst_2 : (i : I) → SMul (f i) (h i)]
  [inst_3 : ∀ (i : I), IsScalarTower (f i) (g i) (h i)], IsScalarTower ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
Pi.isScalarTower''
#align pi.vadd_assoc_class'' Pi.vaddAssocClass'': ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [inst : (i : I) → VAdd (f i) (g i)]
  [inst_1 : (i : I) → VAdd (g i) (h i)] [inst_2 : (i : I) → VAdd (f i) (h i)]
  [inst_3 : ∀ (i : I), VAddAssocClass (f i) (g i) (h i)], VAddAssocClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
Pi.vaddAssocClass''

@[to_additive: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [inst : (i : I) → VAdd α (f i)]
  [inst_1 : (i : I) → VAdd β (f i)] [inst_2 : ∀ (i : I), VAddCommClass α β (f i)], VAddCommClass α β ((i : I) → f i)
to_additive]
instance smulCommClass: ∀ {α : Type ?u.3310} {β : Type ?u.3313} [inst : (i : I) → SMul α (f i)] [inst_1 : (i : I) → SMul β (f i)]
  [inst_2 : ∀ (i : I), SMulCommClass α β (f i)], SMulCommClass α β ((i : I) → f i)
smulCommClass {α: Type ?u.3310
α β: Type ?u.3313
β : Type _: Type (?u.3313+1)
Type _} [∀ i: ?m.3317
i, SMul: Type ?u.3321 → Type ?u.3320 → Type (max?u.3321?u.3320)
SMul α: Type ?u.3310
α <| f: I → Type v
f i: ?m.3317
i] [∀ i: ?m.3326
i, SMul: Type ?u.3330 → Type ?u.3329 → Type (max?u.3330?u.3329)
SMul β: Type ?u.3313
β <| f: I → Type v
f i: ?m.3326
i]
    [∀ i: ?m.3335
i, SMulCommClass: (M : Type ?u.3340) → (N : Type ?u.3339) → (α : Type ?u.3338) → [inst : SMul M α] → [inst : SMul N α] → Prop
SMulCommClass α: Type ?u.3310
α β: Type ?u.3313
β (f: I → Type v
f i: ?m.3335
i)] : SMulCommClass: (M : Type ?u.3376) → (N : Type ?u.3375) → (α : Type ?u.3374) → [inst : SMul M α] → [inst : SMul N α] → Prop
SMulCommClass α: Type ?u.3310
α β: Type ?u.3313
β (∀ i: I
i : I: Type u
I, f: I → Type v
f i: I
i) :=
  ⟨fun x: ?m.3548
x y: ?m.3551
y z: ?m.3554
z => funext: ∀ {α : Sort ?u.3557} {β : α → Sort ?u.3556} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun i: ?m.3571
i => smul_comm: ∀ {M : Type ?u.3575} {N : Type ?u.3574} {α : Type ?u.3573} [inst : SMul M α] [inst_1 : SMul N α]
  [self : SMulCommClass M N α] (m : M) (n : N) (a : α), m • n • a = n • m • a
smul_comm x: ?m.3548
x y: ?m.3551
y (z: ?m.3554
z i: ?m.3571
i)⟩
#align pi.smul_comm_class Pi.smulCommClass: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [inst : (i : I) → SMul α (f i)]
  [inst_1 : (i : I) → SMul β (f i)] [inst_2 : ∀ (i : I), SMulCommClass α β (f i)], SMulCommClass α β ((i : I) → f i)
Pi.smulCommClass
#align pi.vadd_comm_class Pi.vaddCommClass: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [inst : (i : I) → VAdd α (f i)]
  [inst_1 : (i : I) → VAdd β (f i)] [inst_2 : ∀ (i : I), VAddCommClass α β (f i)], VAddCommClass α β ((i : I) → f i)
Pi.vaddCommClass

@[to_additive: ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [inst : (i : I) → VAdd α (g i)]
  [inst_1 : (i : I) → VAdd (f i) (g i)] [inst_2 : ∀ (i : I), VAddCommClass α (f i) (g i)],
  VAddCommClass α ((i : I) → f i) ((i : I) → g i)
to_additive]
instance smulCommClass': ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [inst : (i : I) → SMul α (g i)]
  [inst_1 : (i : I) → SMul (f i) (g i)] [inst_2 : ∀ (i : I), SMulCommClass α (f i) (g i)],
  SMulCommClass α ((i : I) → f i) ((i : I) → g i)
smulCommClass' {g: I → Type ?u.3926
g : I: Type u
I → Type _: Type (?u.3926+1)
Type _} {α: Type ?u.3929
α : Type _: Type (?u.3929+1)
Type _} [∀ i: ?m.3933
i, SMul: Type ?u.3937 → Type ?u.3936 → Type (max?u.3937?u.3936)
SMul α: Type ?u.3929
α <| g: I → Type ?u.3926
g i: ?m.3933
i]
    [∀ i: ?m.3942
i, SMul: Type ?u.3946 → Type ?u.3945 → Type (max?u.3946?u.3945)
SMul (f: I → Type v
f i: ?m.3942
i) (g: I → Type ?u.3926
g i: ?m.3942
i)] [∀ i: ?m.3951
i, SMulCommClass: (M : Type ?u.3956) → (N : Type ?u.3955) → (α : Type ?u.3954) → [inst : SMul M α] → [inst : SMul N α] → Prop
SMulCommClass α: Type ?u.3929
α (f: I → Type v
f i: ?m.3951
i) (g: I → Type ?u.3926
g i: ?m.3951
i)] :
    SMulCommClass: (M : Type ?u.3993) → (N : Type ?u.3992) → (α : Type ?u.3991) → [inst : SMul M α] → [inst : SMul N α] → Prop
SMulCommClass α: Type ?u.3929
α (∀ i: I
i : I: Type u
I, f: I → Type v
f i: I
i) (∀ i: I
i : I: Type u
I, g: I → Type ?u.3926
g i: I
i) :=
  ⟨fun x: ?m.4182
x y: ?m.4185
y z: ?m.4188
z => funext: ∀ {α : Sort ?u.4192} {β : α → Sort ?u.4191} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun i: ?m.4206
i => smul_comm: ∀ {M : Type ?u.4210} {N : Type ?u.4209} {α : Type ?u.4208} [inst : SMul M α] [inst_1 : SMul N α]
  [self : SMulCommClass M N α] (m : M) (n : N) (a : α), m • n • a = n • m • a
smul_comm x: ?m.4182
x (y: ?m.4185
y i: ?m.4206
i) (z: ?m.4188
z i: ?m.4206
i)⟩
#align pi.smul_comm_class' Pi.smulCommClass': ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [inst : (i : I) → SMul α (g i)]
  [inst_1 : (i : I) → SMul (f i) (g i)] [inst_2 : ∀ (i : I), SMulCommClass α (f i) (g i)],
  SMulCommClass α ((i : I) → f i) ((i : I) → g i)
Pi.smulCommClass'
#align pi.vadd_comm_class' Pi.vaddCommClass': ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [inst : (i : I) → VAdd α (g i)]
  [inst_1 : (i : I) → VAdd (f i) (g i)] [inst_2 : ∀ (i : I), VAddCommClass α (f i) (g i)],
  VAddCommClass α ((i : I) → f i) ((i : I) → g i)
Pi.vaddCommClass'

@[to_additive: ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [inst : (i : I) → VAdd (g i) (h i)]
  [inst_1 : (i : I) → VAdd (f i) (h i)] [inst_2 : ∀ (i : I), VAddCommClass (f i) (g i) (h i)],
  VAddCommClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
to_additive]
instance smulCommClass'': ∀ {g : I → Type ?u.4586} {h : I → Type ?u.4591} [inst : (i : I) → SMul (g i) (h i)]
  [inst_1 : (i : I) → SMul (f i) (h i)] [inst_2 : ∀ (i : I), SMulCommClass (f i) (g i) (h i)],
  SMulCommClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
smulCommClass'' {g: I → Type ?u.4586
g : I: Type u
I → Type _: Type (?u.4586+1)
Type _} {h: I → Type ?u.4591
h : I: Type u
I → Type _: Type (?u.4591+1)
Type _} [∀ i: ?m.4595
i, SMul: Type ?u.4599 → Type ?u.4598 → Type (max?u.4599?u.4598)
SMul (g: I → Type ?u.4586
g i: ?m.4595
i) (h: I → Type ?u.4591
h i: ?m.4595
i)]
    [∀ i: ?m.4604
i, SMul: Type ?u.4608 → Type ?u.4607 → Type (max?u.4608?u.4607)
SMul (f: I → Type v
f i: ?m.4604
i) (h: I → Type ?u.4591
h i: ?m.4604
i)] [∀ i: ?m.4613
i, SMulCommClass: (M : Type ?u.4618) → (N : Type ?u.4617) → (α : Type ?u.4616) → [inst : SMul M α] → [inst : SMul N α] → Prop
SMulCommClass (f: I → Type v
f i: ?m.4613
i) (g: I → Type ?u.4586
g i: ?m.4613
i) (h: I → Type ?u.4591
h i: ?m.4613
i)] :
    SMulCommClass: (M : Type ?u.4656) → (N : Type ?u.4655) → (α : Type ?u.4654) → [inst : SMul M α] → [inst : SMul N α] → Prop
SMulCommClass (∀ i: ?m.4658
i, f: I → Type v
f i: ?m.4658
i) (∀ i: ?m.4663
i, g: I → Type ?u.4586
g i: ?m.4663
i) (∀ i: ?m.4668
i, h: I → Type ?u.4591
h i: ?m.4668
i) :=
  ⟨fun x: ?m.4863
x y: ?m.4866
y z: ?m.4870
z => funext: ∀ {α : Sort ?u.4874} {β : α → Sort ?u.4873} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun i: ?m.4888
i => smul_comm: ∀ {M : Type ?u.4892} {N : Type ?u.4891} {α : Type ?u.4890} [inst : SMul M α] [inst_1 : SMul N α]
  [self : SMulCommClass M N α] (m : M) (n : N) (a : α), m • n • a = n • m • a
smul_comm (x: ?m.4863
x i: ?m.4888
i) (y: ?m.4866
y i: ?m.4888
i) (z: ?m.4870
z i: ?m.4888
i)⟩
#align pi.smul_comm_class'' Pi.smulCommClass'': ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [inst : (i : I) → SMul (g i) (h i)]
  [inst_1 : (i : I) → SMul (f i) (h i)] [inst_2 : ∀ (i : I), SMulCommClass (f i) (g i) (h i)],
  SMulCommClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
Pi.smulCommClass''
#align pi.vadd_comm_class'' Pi.vaddCommClass'': ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [inst : (i : I) → VAdd (g i) (h i)]
  [inst_1 : (i : I) → VAdd (f i) (h i)] [inst_2 : ∀ (i : I), VAddCommClass (f i) (g i) (h i)],
  VAddCommClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
Pi.vaddCommClass''

@[to_additive: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → VAdd α (f i)] [inst_1 : (i : I) → VAdd αᵃᵒᵖ (f i)]
  [inst_2 : ∀ (i : I), IsCentralVAdd α (f i)], IsCentralVAdd α ((i : I) → f i)
to_additive]
instance isCentralScalar: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → SMul α (f i)] [inst_1 : (i : I) → SMul αᵐᵒᵖ (f i)]
  [inst_2 : ∀ (i : I), IsCentralScalar α (f i)], IsCentralScalar α ((i : I) → f i)
isCentralScalar {α: Type ?u.5289
α : Type _: Type (?u.5289+1)
Type _} [∀ i: ?m.5293
i, SMul: Type ?u.5297 → Type ?u.5296 → Type (max?u.5297?u.5296)
SMul α: Type ?u.5289
α <| f: I → Type v
f i: ?m.5293
i] [∀ i: ?m.5302
i, SMul: Type ?u.5306 → Type ?u.5305 → Type (max?u.5306?u.5305)
SMul α: Type ?u.5289
αᵐᵒᵖ <| f: I → Type v
f i: ?m.5302
i]
    [∀ i: ?m.5312
i, IsCentralScalar: (M : Type ?u.5316) → (α : Type ?u.5315) → [inst : SMul M α] → [inst : SMul Mᵐᵒᵖ α] → Prop
IsCentralScalar α: Type ?u.5289
α (f: I → Type v
f i: ?m.5312
i)] : IsCentralScalar: (M : Type ?u.5347) → (α : Type ?u.5346) → [inst : SMul M α] → [inst : SMul Mᵐᵒᵖ α] → Prop
IsCentralScalar α: Type ?u.5289
α (∀ i: ?m.5349
i, f: I → Type v
f i: ?m.5349
i) :=
  ⟨fun _: ?m.5501
_ _: ?m.5504
_ => funext: ∀ {α : Sort ?u.5507} {β : α → Sort ?u.5506} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun _: ?m.5521
_ => op_smul_eq_smul: ∀ {M : Type ?u.5524} {α : Type ?u.5523} [inst : SMul M α] [inst_1 : SMul Mᵐᵒᵖ α] [self : IsCentralScalar M α] (m : M)
  (a : α), MulOpposite.op m • a = m • a
op_smul_eq_smul _: ?m.5525
_ _: ?m.5526
_⟩

/-- If `f i` has a faithful scalar action for a given `i`, then so does `Π i, f i`. This is
not an instance as `i` cannot be inferred. -/
@[to_additive: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → VAdd α (f i)] [inst_1 : ∀ (i : I), Nonempty (f i)]
  (i : I) [inst_2 : FaithfulVAdd α (f i)], FaithfulVAdd α ((i : I) → f i)
to_additive
  "If `f i` has a faithful additive action for a given `i`, then
  so does `Π i, f i`. This is not an instance as `i` cannot be inferred"]
theorem faithfulSMul_at: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → SMul α (f i)] [inst_1 : ∀ (i : I), Nonempty (f i)]
  (i : I) [inst_2 : FaithfulSMul α (f i)], FaithfulSMul α ((i : I) → f i)
faithfulSMul_at {α: Type u_1
α : Type _: Type (?u.5902+1)
Type _} [∀ i: ?m.5906
i, SMul: Type ?u.5910 → Type ?u.5909 → Type (max?u.5910?u.5909)
SMul α: Type ?u.5902
α <| f: I → Type v
f i: ?m.5906
i] [∀ i: ?m.5915
i, Nonempty: Sort ?u.5918 → Prop
Nonempty (f: I → Type v
f i: ?m.5915
i)] (i: I
i : I: Type u
I)
    [FaithfulSMul: (M : Type ?u.5925) → (α : Type ?u.5924) → [inst : SMul M α] → Prop
FaithfulSMul α: Type ?u.5902
α (f: I → Type v
f i: I
i)] : FaithfulSMul: (M : Type ?u.5943) → (α : Type ?u.5942) → [inst : SMul M α] → Prop
FaithfulSMul α: Type ?u.5902
α (∀ i: ?m.5945
i, f: I → Type v
f i: ?m.5945
i) :=
  ⟨fun h: ?m.6038
h =>
    eq_of_smul_eq_smul: ∀ {M : Type ?u.6042} {α : Type ?u.6041} [inst : SMul M α] [self : FaithfulSMul M α] {m₁ m₂ : M},
  (∀ (a : α), m₁ • a = m₂ • a) → m₁ = m₂
eq_of_smul_eq_smul fun a: f i
a : f: I → Type v
f i: I
i => by
Goals accomplished! 🐙
      I: Type u

f: I → Type v

x, y: (i : I) → f i

i✝: I

α: Type u_1

inst✝²: (i : I) → SMul α (f i)

inst✝¹: ∀ (i : I), Nonempty (f i)

i: I

inst✝: FaithfulSMul α (f i)

m₁✝, m₂✝: α

h: ∀ (a : (i : I) → f i), m₁✝ • a = m₂✝ • a

a: f i

m₁✝ • a = m₂✝ • aclassical
        I: Type u

f: I → Type v

x, y: (i : I) → f i

i✝: I

α: Type u_1

inst✝²: (i : I) → SMul α (f i)

inst✝¹: ∀ (i : I), Nonempty (f i)

i: I

inst✝: FaithfulSMul α (f i)

m₁✝, m₂✝: α

h: ∀ (a : (i : I) → f i), m₁✝ • a = m₂✝ • a

a: f i

m₁✝ • a = m₂✝ • ahave :=
          congr_fun: ∀ {α : Sort ?u.6162} {β : α → Sort ?u.6161} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
congr_fun (h: ∀ (a : (i : I) → f i), m₁✝ • a = m₂✝ • a
h <| Function.update: {α : Sort ?u.6168} → {β : α → Sort ?u.6167} → [inst : DecidableEq α] → ((a : α) → β a) → (a' : α) → β a' → (a : α) → β a
Function.update (fun j: ?m.6223
j => Classical.choice: {α : Sort ?u.6225} → Nonempty α → α
Classical.choice (‹∀ i, Nonempty (f i)› j: ?m.6223
j)) i: I
i a: f i
a)
            i: I
iI: Type u

f: I → Type v

x, y: (i : I) → f i

i✝: I

α: Type u_1

inst✝²: (i : I) → SMul α (f i)

inst✝¹: ∀ (i : I), Nonempty (f i)

i: I

inst✝: FaithfulSMul α (f i)

m₁✝, m₂✝: α

h: ∀ (a : (i : I) → f i), m₁✝ • a = m₂✝ • a

a: f i

this: (m₁✝ • Function.update (fun j => Classical.choice (_ : Nonempty (f j))) i a) i =   (m₂✝ • Function.update (fun j => Classical.choice (_ : Nonempty (f j))) i a) i

m₁✝ • a = m₂✝ • a
        I: Type u

f: I → Type v

x, y: (i : I) → f i

i✝: I

α: Type u_1

inst✝²: (i : I) → SMul α (f i)

inst✝¹: ∀ (i : I), Nonempty (f i)

i: I

inst✝: FaithfulSMul α (f i)

m₁✝, m₂✝: α

h: ∀ (a : (i : I) → f i), m₁✝ • a = m₂✝ • a

a: f i

m₁✝ • a = m₂✝ • asimpa using this: ?m.6160
this
Goals accomplished! 🐙⟩
#align pi.has_faithful_smul_at Pi.faithfulSMul_at: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → SMul α (f i)] [inst_1 : ∀ (i : I), Nonempty (f i)]
  (i : I) [inst_2 : FaithfulSMul α (f i)], FaithfulSMul α ((i : I) → f i)
Pi.faithfulSMul_at
#align pi.has_faithful_vadd_at Pi.faithfulVAdd_at: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → VAdd α (f i)] [inst_1 : ∀ (i : I), Nonempty (f i)]
  (i : I) [inst_2 : FaithfulVAdd α (f i)], FaithfulVAdd α ((i : I) → f i)
Pi.faithfulVAdd_at

@[to_additive: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : Nonempty I] [inst : (i : I) → VAdd α (f i)]
  [inst_1 : ∀ (i : I), Nonempty (f i)] [inst_2 : ∀ (i : I), FaithfulVAdd α (f i)], FaithfulVAdd α ((i : I) → f i)
to_additive]
instance faithfulSMul: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : Nonempty I] [inst : (i : I) → SMul α (f i)]
  [inst_1 : ∀ (i : I), Nonempty (f i)] [inst_2 : ∀ (i : I), FaithfulSMul α (f i)], FaithfulSMul α ((i : I) → f i)
faithfulSMul {α: Type ?u.7332
α : Type _: Type (?u.7332+1)
Type _} [Nonempty: Sort ?u.7335 → Prop
Nonempty I: Type u
I] [∀ i: ?m.7339
i, SMul: Type ?u.7343 → Type ?u.7342 → Type (max?u.7343?u.7342)
SMul α: Type ?u.7332
α <| f: I → Type v
f i: ?m.7339
i] [∀ i: ?m.7348
i, Nonempty: Sort ?u.7351 → Prop
Nonempty (f: I → Type v
f i: ?m.7348
i)]
    [∀ i: ?m.7356
i, FaithfulSMul: (M : Type ?u.7360) → (α : Type ?u.7359) → [inst : SMul M α] → Prop
FaithfulSMul α: Type ?u.7332
α (f: I → Type v
f i: ?m.7356
i)] : FaithfulSMul: (M : Type ?u.7379) → (α : Type ?u.7378) → [inst : SMul M α] → Prop
FaithfulSMul α: Type ?u.7332
α (∀ i: ?m.7381
i, f: I → Type v
f i: ?m.7381
i) :=
  let ⟨i: I
i⟩ := ‹Nonempty I›
  faithfulSMul_at: ∀ {I : Type ?u.7459} {f : I → Type ?u.7458} {α : Type ?u.7460} [inst : (i : I) → SMul α (f i)]
  [inst_1 : ∀ (i : I), Nonempty (f i)] (i : I) [inst_2 : FaithfulSMul α (f i)], FaithfulSMul α ((i : I) → f i)
faithfulSMul_at i: I
i
#align pi.has_faithful_smul Pi.faithfulSMul: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : Nonempty I] [inst : (i : I) → SMul α (f i)]
  [inst_1 : ∀ (i : I), Nonempty (f i)] [inst_2 : ∀ (i : I), FaithfulSMul α (f i)], FaithfulSMul α ((i : I) → f i)
Pi.faithfulSMul
#align pi.has_faithful_vadd Pi.faithfulVAdd: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : Nonempty I] [inst : (i : I) → VAdd α (f i)]
  [inst_1 : ∀ (i : I), Nonempty (f i)] [inst_2 : ∀ (i : I), FaithfulVAdd α (f i)], FaithfulVAdd α ((i : I) → f i)
Pi.faithfulVAdd

@[to_additive: {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) → {m : AddMonoid α} → [inst : (i : I) → AddAction α (f i)] → AddAction α ((i : I) → f i)
to_additive]
instance mulAction: {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) → {m : Monoid α} → [inst : (i : I) → MulAction α (f i)] → MulAction α ((i : I) → f i)
mulAction (α: ?m.7842
α) {m: Monoid α
m : Monoid: Type ?u.7845 → Type ?u.7845
Monoid α: ?m.7842
α} [∀ i: ?m.7849
i, MulAction: (α : Type ?u.7853) → Type ?u.7852 → [inst : Monoid α] → Type (max?u.7853?u.7852)
MulAction α: ?m.7842
α <| f: I → Type v
f i: ?m.7849
i] :
    @MulAction: (α : Type ?u.7866) → Type ?u.7865 → [inst : Monoid α] → Type (max?u.7866?u.7865)
MulAction α: ?m.7842
α (∀ i: I
i : I: Type u
I, f: I → Type v
f i: I
i) m: Monoid α
m where
  smul := (· • ·): α → ((i : I) → f i) → (i : I) → f i
(· • ·)
  mul_smul _: ?m.8878
_ _: ?m.8881
_ _: ?m.8884
_ := funext: ∀ {α : Sort ?u.8887} {β : α → Sort ?u.8886} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun _: ?m.8897
_ => mul_smul: ∀ {α : Type ?u.8900} {β : Type ?u.8899} [inst : Monoid α] [self : MulAction α β] (x y : α) (b : β),
  (x * y) • b = x • y • b
mul_smul _: ?m.8901
_ _: ?m.8901
_ _: ?m.8902
_
  one_smul _: ?m.8810
_ := funext: ∀ {α : Sort ?u.8813} {β : α → Sort ?u.8812} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun _: ?m.8827
_ => one_smul: ∀ (M : Type ?u.8830) {α : Type ?u.8829} [inst : Monoid M] [inst_1 : MulAction M α] (b : α), 1 • b = b
one_smul α: Type ?u.7845
α _: ?m.8831
_
#align pi.mul_action Pi.mulAction: {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) → {m : Monoid α} → [inst : (i : I) → MulAction α (f i)] → MulAction α ((i : I) → f i)
Pi.mulAction
#align pi.add_action Pi.addAction: {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) → {m : AddMonoid α} → [inst : (i : I) → AddAction α (f i)] → AddAction α ((i : I) → f i)
Pi.addAction

@[to_additive: {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {m : (i : I) → AddMonoid (f i)} →
        [inst : (i : I) → AddAction (f i) (g i)] → AddAction ((i : I) → f i) ((i : I) → g i)
to_additive]
instance mulAction': {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {m : (i : I) → Monoid (f i)} →
        [inst : (i : I) → MulAction (f i) (g i)] → MulAction ((i : I) → f i) ((i : I) → g i)
mulAction' {g: I → Type ?u.9383
g : I: Type u
I → Type _: Type (?u.9383+1)
Type _} {m: (i : I) → Monoid (f i)
m : ∀ i: ?m.9387
i, Monoid: Type ?u.9390 → Type ?u.9390
Monoid (f: I → Type v
f i: ?m.9387
i)} [∀ i: ?m.9394
i, MulAction: (α : Type ?u.9398) → Type ?u.9397 → [inst : Monoid α] → Type (max?u.9398?u.9397)
MulAction (f: I → Type v
f i: ?m.9394
i) (g: I → Type ?u.9383
g i: ?m.9394
i)] :
    @MulAction: (α : Type ?u.9415) → Type ?u.9414 → [inst : Monoid α] → Type (max?u.9415?u.9414)
MulAction (∀ i: ?m.9417
i, f: I → Type v
f i: ?m.9417
i) (∀ i: I
i : I: Type u
I, g: I → Type ?u.9383
g i: I
i)
      (@Pi.monoid: {I : Type ?u.9426} → {f : I → Type ?u.9425} → [inst : (i : I) → Monoid (f i)] → Monoid ((i : I) → f i)
Pi.monoid I: Type u
I f: I → Type v
f m: (i : I) → Monoid (f i)
m) where
  smul := (· • ·): ((i : I) → f i) → ((i : I) → g i) → (i : I) → g i
(· • ·)
  mul_smul _: ?m.10614
_ _: ?m.10617
_ _: ?m.10620
_ := funext: ∀ {α : Sort ?u.10624} {β : α → Sort ?u.10623} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun _: ?m.10635
_ => mul_smul: ∀ {α : Type ?u.10638} {β : Type ?u.10637} [inst : Monoid α] [self : MulAction α β] (x y : α) (b : β),
  (x * y) • b = x • y • b
mul_smul _: ?m.10639
_ _: ?m.10639
_ _: ?m.10640
_
  one_smul _: ?m.10514
_ := funext: ∀ {α : Sort ?u.10518} {β : α → Sort ?u.10517} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun _: ?m.10532
_ => one_smul: ∀ (M : Type ?u.10535) {α : Type ?u.10534} [inst : Monoid M] [inst_1 : MulAction M α] (b : α), 1 • b = b
one_smul _: Type ?u.10535
_ _: ?m.10537
_
#align pi.mul_action' Pi.mulAction': {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {m : (i : I) → Monoid (f i)} →
        [inst : (i : I) → MulAction (f i) (g i)] → MulAction ((i : I) → f i) ((i : I) → g i)
Pi.mulAction'
#align pi.add_action' Pi.addAction': {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {m : (i : I) → AddMonoid (f i)} →
        [inst : (i : I) → AddAction (f i) (g i)] → AddAction ((i : I) → f i) ((i : I) → g i)
Pi.addAction'

instance smulZeroClass: {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) →
      {n : (i : I) → Zero (f i)} → [inst : (i : I) → SMulZeroClass α (f i)] → SMulZeroClass α ((i : I) → f i)
smulZeroClass (α: ?m.11191
α) {n: (i : I) → Zero (f i)
n : ∀ i: ?m.11195
i, Zero: Type ?u.11198 → Type ?u.11198
Zero <| f: I → Type v
f i: ?m.11195
i} [∀ i: ?m.11202
i, SMulZeroClass: Type ?u.11206 → (A : Type ?u.11205) → [inst : Zero A] → Type (max?u.11206?u.11205)
SMulZeroClass α: ?m.11191
α <| f: I → Type v
f i: ?m.11202
i] :
  @SMulZeroClass: Type ?u.11229 → (A : Type ?u.11228) → [inst : Zero A] → Type (max?u.11229?u.11228)
SMulZeroClass α: ?m.11191
α (∀ i: I
i : I: Type u
I, f: I → Type v
f i: I
i) (@Pi.instZero: {I : Type ?u.11235} → {f : I → Type ?u.11234} → [inst : (i : I) → Zero (f i)] → Zero ((i : I) → f i)
Pi.instZero I: Type u
I f: I → Type v
f n: (i : I) → Zero (f i)
n) where
  smul_zero _: ?m.11384
_ := funext: ∀ {α : Sort ?u.11387} {β : α → Sort ?u.11386} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun _: ?m.11401
_ => smul_zero: ∀ {M : Type ?u.11404} {A : Type ?u.11403} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0
smul_zero _: ?m.11405
_
#align pi.smul_zero_class Pi.smulZeroClass: {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) →
      {n : (i : I) → Zero (f i)} → [inst : (i : I) → SMulZeroClass α (f i)] → SMulZeroClass α ((i : I) → f i)
Pi.smulZeroClass

instance smulZeroClass': {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {n : (i : I) → Zero (g i)} →
        [inst : (i : I) → SMulZeroClass (f i) (g i)] → SMulZeroClass ((i : I) → f i) ((i : I) → g i)
smulZeroClass' {g: I → Type ?u.11626
g : I: Type u
I → Type _: Type (?u.11626+1)
Type _} {n: (i : I) → Zero (g i)
n : ∀ i: ?m.11630
i, Zero: Type ?u.11633 → Type ?u.11633
Zero <| g: I → Type ?u.11626
g i: ?m.11630
i} [∀ i: ?m.11637
i, SMulZeroClass: Type ?u.11641 → (A : Type ?u.11640) → [inst : Zero A] → Type (max?u.11641?u.11640)
SMulZeroClass (f: I → Type v
f i: ?m.11637
i) (g: I → Type ?u.11626
g i: ?m.11637
i)] :
  @SMulZeroClass: Type ?u.11664 → (A : Type ?u.11663) → [inst : Zero A] → Type (max?u.11664?u.11663)
SMulZeroClass (∀ i: ?m.11666
i, f: I → Type v
f i: ?m.11666
i) (∀ i: I
i : I: Type u
I, g: I → Type ?u.11626
g i: I
i) (@Pi.instZero: {I : Type ?u.11675} → {f : I → Type ?u.11674} → [inst : (i : I) → Zero (f i)] → Zero ((i : I) → f i)
Pi.instZero I: Type u
I g: I → Type ?u.11626
g n: (i : I) → Zero (g i)
n) where
  smul_zero := by
Goals accomplished! 🐙 I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.11626

n: (i : I) → Zero (g i)

inst✝: (i : I) → SMulZeroClass (f i) (g i)

∀ (a : (i : I) → f i), a • 0 = 0introsI: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.11626

n: (i : I) → Zero (g i)

inst✝: (i : I) → SMulZeroClass (f i) (g i)

a✝: (i : I) → f i

a✝ • 0 = 0;I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.11626

n: (i : I) → Zero (g i)

inst✝: (i : I) → SMulZeroClass (f i) (g i)

a✝: (i : I) → f i

a✝ • 0 = 0 I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.11626

n: (i : I) → Zero (g i)

inst✝: (i : I) → SMulZeroClass (f i) (g i)

∀ (a : (i : I) → f i), a • 0 = 0ext x: ?α
xI: Type u

f: I → Type v

x✝, y: (i : I) → f i

i: I

g: I → Type ?u.11626

n: (i : I) → Zero (g i)

inst✝: (i : I) → SMulZeroClass (f i) (g i)

a✝: (i : I) → f i

x: I

h(a✝ • 0) x = OfNat.ofNat 0 x;I: Type u

f: I → Type v

x✝, y: (i : I) → f i

i: I

g: I → Type ?u.11626

n: (i : I) → Zero (g i)

inst✝: (i : I) → SMulZeroClass (f i) (g i)

a✝: (i : I) → f i

x: I

h(a✝ • 0) x = OfNat.ofNat 0 x I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.11626

n: (i : I) → Zero (g i)

inst✝: (i : I) → SMulZeroClass (f i) (g i)

∀ (a : (i : I) → f i), a • 0 = 0exact smul_zero: ∀ {M : Type ?u.11888} {A : Type ?u.11887} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0
smul_zero _: ?m.11889
_
Goals accomplished! 🐙
#align pi.smul_zero_class' Pi.smulZeroClass': {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {n : (i : I) → Zero (g i)} →
        [inst : (i : I) → SMulZeroClass (f i) (g i)] → SMulZeroClass ((i : I) → f i) ((i : I) → g i)
Pi.smulZeroClass'

instance distribSMul: (α : Type ?u.12128) →
  {n : (i : I) → AddZeroClass (f i)} → [inst : (i : I) → DistribSMul α (f i)] → DistribSMul α ((i : I) → f i)
distribSMul (α: ?m.12113
α) {n: (i : I) → AddZeroClass (f i)
n : ∀ i: ?m.12117
i, AddZeroClass: Type ?u.12120 → Type ?u.12120
AddZeroClass <| f: I → Type v
f i: ?m.12117
i} [∀ i: ?m.12124
i, DistribSMul: Type ?u.12128 → (A : Type ?u.12127) → [inst : AddZeroClass A] → Type (max?u.12128?u.12127)
DistribSMul α: ?m.12113
α <| f: I → Type v
f i: ?m.12124
i] :
  @DistribSMul: Type ?u.12141 → (A : Type ?u.12140) → [inst : AddZeroClass A] → Type (max?u.12141?u.12140)
DistribSMul α: ?m.12113
α (∀ i: I
i : I: Type u
I, f: I → Type v
f i: I
i) (@Pi.addZeroClass: {I : Type ?u.12147} → {f : I → Type ?u.12146} → [inst : (i : I) → AddZeroClass (f i)] → AddZeroClass ((i : I) → f i)
Pi.addZeroClass I: Type u
I f: I → Type v
f n: (i : I) → AddZeroClass (f i)
n) where
  smul_zero _: ?m.13696
_ := funext: ∀ {α : Sort ?u.13699} {β : α → Sort ?u.13698} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun _: ?m.13713
_ => smul_zero: ∀ {M : Type ?u.13716} {A : Type ?u.13715} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0
smul_zero _: ?m.13717
_
  smul_add _: ?m.14067
_ _: ?m.14070
_ _: ?m.14073
_ := funext: ∀ {α : Sort ?u.14076} {β : α → Sort ?u.14075} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun _: ?m.14086
_ => smul_add: ∀ {M : Type ?u.14089} {A : Type ?u.14088} [inst : AddZeroClass A] [inst_1 : DistribSMul M A] (a : M) (b₁ b₂ : A),
  a • (b₁ + b₂) = a • b₁ + a • b₂
smul_add _: ?m.14090
_ _: ?m.14091
_ _: ?m.14091
_
#align pi.distrib_smul Pi.distribSMul: {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) →
      {n : (i : I) → AddZeroClass (f i)} → [inst : (i : I) → DistribSMul α (f i)] → DistribSMul α ((i : I) → f i)
Pi.distribSMul

instance distribSMul': {g : I → Type ?u.14402} →
  {n : (i : I) → AddZeroClass (g i)} →
    [inst : (i : I) → DistribSMul (f i) (g i)] → DistribSMul ((i : I) → f i) ((i : I) → g i)
distribSMul' {g: I → Type ?u.14402
g : I: Type u
I → Type _: Type (?u.14402+1)
Type _} {n: (i : I) → AddZeroClass (g i)
n : ∀ i: ?m.14406
i, AddZeroClass: Type ?u.14409 → Type ?u.14409
AddZeroClass <| g: I → Type ?u.14402
g i: ?m.14406
i}
  [∀ i: ?m.14413
i, DistribSMul: Type ?u.14417 → (A : Type ?u.14416) → [inst : AddZeroClass A] → Type (max?u.14417?u.14416)
DistribSMul (f: I → Type v
f i: ?m.14413
i) (g: I → Type ?u.14402
g i: ?m.14413
i)] :
  @DistribSMul: Type ?u.14430 → (A : Type ?u.14429) → [inst : AddZeroClass A] → Type (max?u.14430?u.14429)
DistribSMul (∀ i: ?m.14432
i, f: I → Type v
f i: ?m.14432
i) (∀ i: I
i : I: Type u
I, g: I → Type ?u.14402
g i: I
i) (@Pi.addZeroClass: {I : Type ?u.14441} → {f : I → Type ?u.14440} → [inst : (i : I) → AddZeroClass (f i)] → AddZeroClass ((i : I) → f i)
Pi.addZeroClass I: Type u
I g: I → Type ?u.14402
g n: (i : I) → AddZeroClass (g i)
n) where
  smul_zero := by
Goals accomplished! 🐙 I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.14402

n: (i : I) → AddZeroClass (g i)

inst✝: (i : I) → DistribSMul (f i) (g i)

∀ (a : (i : I) → f i), a • 0 = 0introsI: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.14402

n: (i : I) → AddZeroClass (g i)

inst✝: (i : I) → DistribSMul (f i) (g i)

a✝: (i : I) → f i

a✝ • 0 = 0;I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.14402

n: (i : I) → AddZeroClass (g i)

inst✝: (i : I) → DistribSMul (f i) (g i)

a✝: (i : I) → f i

a✝ • 0 = 0 I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.14402

n: (i : I) → AddZeroClass (g i)

inst✝: (i : I) → DistribSMul (f i) (g i)

∀ (a : (i : I) → f i), a • 0 = 0ext x: ?α
xI: Type u

f: I → Type v

x✝, y: (i : I) → f i

i: I

g: I → Type ?u.14402

n: (i : I) → AddZeroClass (g i)

inst✝: (i : I) → DistribSMul (f i) (g i)

a✝: (i : I) → f i

x: I

h(a✝ • 0) x = OfNat.ofNat 0 x;I: Type u

f: I → Type v

x✝, y: (i : I) → f i

i: I

g: I → Type ?u.14402

n: (i : I) → AddZeroClass (g i)

inst✝: (i : I) → DistribSMul (f i) (g i)

a✝: (i : I) → f i

x: I

h(a✝ • 0) x = OfNat.ofNat 0 x I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.14402

n: (i : I) → AddZeroClass (g i)

inst✝: (i : I) → DistribSMul (f i) (g i)

∀ (a : (i : I) → f i), a • 0 = 0exact smul_zero: ∀ {M : Type ?u.16244} {A : Type ?u.16243} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0
smul_zero _: ?m.16245
_
Goals accomplished! 🐙
  smul_add := by
Goals accomplished! 🐙 I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.14402

n: (i : I) → AddZeroClass (g i)

inst✝: (i : I) → DistribSMul (f i) (g i)

∀ (a : (i : I) → f i) (x y : (i : I) → g i), a • (x + y) = a • x + a • yintrosI: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.14402

n: (i : I) → AddZeroClass (g i)

inst✝: (i : I) → DistribSMul (f i) (g i)

a✝: (i : I) → f i

x✝, y✝: (i : I) → g i

a✝ • (x✝ + y✝) = a✝ • x✝ + a✝ • y✝;I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.14402

n: (i : I) → AddZeroClass (g i)

inst✝: (i : I) → DistribSMul (f i) (g i)

a✝: (i : I) → f i

x✝, y✝: (i : I) → g i

a✝ • (x✝ + y✝) = a✝ • x✝ + a✝ • y✝ I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.14402

n: (i : I) → AddZeroClass (g i)

inst✝: (i : I) → DistribSMul (f i) (g i)

∀ (a : (i : I) → f i) (x y : (i : I) → g i), a • (x + y) = a • x + a • yext x: ?α
xI: Type u

f: I → Type v

x✝¹, y: (i : I) → f i

i: I

g: I → Type ?u.14402

n: (i : I) → AddZeroClass (g i)

inst✝: (i : I) → DistribSMul (f i) (g i)

a✝: (i : I) → f i

x✝, y✝: (i : I) → g i

x: I

h(a✝ • (x✝ + y✝)) x = (a✝ • x✝ + a✝ • y✝) x;I: Type u

f: I → Type v

x✝¹, y: (i : I) → f i

i: I

g: I → Type ?u.14402

n: (i : I) → AddZeroClass (g i)

inst✝: (i : I) → DistribSMul (f i) (g i)

a✝: (i : I) → f i

x✝, y✝: (i : I) → g i

x: I

h(a✝ • (x✝ + y✝)) x = (a✝ • x✝ + a✝ • y✝) x I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.14402

n: (i : I) → AddZeroClass (g i)

inst✝: (i : I) → DistribSMul (f i) (g i)

∀ (a : (i : I) → f i) (x y : (i : I) → g i), a • (x + y) = a • x + a • yexact smul_add: ∀ {M : Type ?u.16627} {A : Type ?u.16626} [inst : AddZeroClass A] [inst_1 : DistribSMul M A] (a : M) (b₁ b₂ : A),
  a • (b₁ + b₂) = a • b₁ + a • b₂
smul_add _: ?m.16628
_ _: ?m.16629
_ _: ?m.16629
_
Goals accomplished! 🐙
#align pi.distrib_smul' Pi.distribSMul': {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {n : (i : I) → AddZeroClass (g i)} →
        [inst : (i : I) → DistribSMul (f i) (g i)] → DistribSMul ((i : I) → f i) ((i : I) → g i)
Pi.distribSMul'

instance distribMulAction: (α : Type ?u.16943) →
  {m : Monoid α} →
    {n : (i : I) → AddMonoid (f i)} → [inst : (i : I) → DistribMulAction α (f i)] → DistribMulAction α ((i : I) → f i)
distribMulAction (α: Type ?u.16943
α) {m: Monoid α
m : Monoid: Type ?u.16943 → Type ?u.16943
Monoid α: ?m.16940
α} {n: (i : I) → AddMonoid (f i)
n : ∀ i: ?m.16947
i, AddMonoid: Type ?u.16950 → Type ?u.16950
AddMonoid <| f: I → Type v
f i: ?m.16947
i}
    [∀ i: ?m.16954
i, DistribMulAction: (M : Type ?u.16958) → (A : Type ?u.16957) → [inst : Monoid M] → [inst : AddMonoid A] → Type (max?u.16958?u.16957)
DistribMulAction α: ?m.16940
α <| f: I → Type v
f i: ?m.16954
i] : @DistribMulAction: (M : Type ?u.16983) → (A : Type ?u.16982) → [inst : Monoid M] → [inst : AddMonoid A] → Type (max?u.16983?u.16982)
DistribMulAction α: ?m.16940
α (∀ i: I
i : I: Type u
I, f: I → Type v
f i: I
i) m: Monoid α
m (@Pi.addMonoid: {I : Type ?u.16989} → {f : I → Type ?u.16988} → [inst : (i : I) → AddMonoid (f i)] → AddMonoid ((i : I) → f i)
Pi.addMonoid I: Type u
I f: I → Type v
f n: (i : I) → AddMonoid (f i)
n) :=
  { Pi.mulAction _, Pi.distribSMul _ with }: DistribMulAction ?m.17115 ?m.17116
{ Pi.mulAction: {I : Type ?u.17007} →
  {f : I → Type ?u.17006} →
    (α : Type ?u.17005) → {m : Monoid α} → [inst : (i : I) → MulAction α (f i)] → MulAction α ((i : I) → f i)
Pi.mulAction{ Pi.mulAction _, Pi.distribSMul _ with }: DistribMulAction ?m.17115 ?m.17116
 _: Type ?u.17005
_{ Pi.mulAction _, Pi.distribSMul _ with }: DistribMulAction ?m.17115 ?m.17116
, Pi.distribSMul: {I : Type ?u.17067} →
  {f : I → Type ?u.17066} →
    (α : Type ?u.17065) →
      {n : (i : I) → AddZeroClass (f i)} → [inst : (i : I) → DistribSMul α (f i)] → DistribSMul α ((i : I) → f i)
Pi.distribSMul{ Pi.mulAction _, Pi.distribSMul _ with }: DistribMulAction ?m.17115 ?m.17116
 _: Type ?u.17065
_{ Pi.mulAction _, Pi.distribSMul _ with }: DistribMulAction ?m.17115 ?m.17116
 { Pi.mulAction _, Pi.distribSMul _ with }: DistribMulAction ?m.17115 ?m.17116
with{ Pi.mulAction _, Pi.distribSMul _ with }: DistribMulAction ?m.17115 ?m.17116
 }
#align pi.distrib_mul_action Pi.distribMulAction: {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) →
      {m : Monoid α} →
        {n : (i : I) → AddMonoid (f i)} →
          [inst : (i : I) → DistribMulAction α (f i)] → DistribMulAction α ((i : I) → f i)
Pi.distribMulAction

instance distribMulAction': {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {m : (i : I) → Monoid (f i)} →
        {n : (i : I) → AddMonoid (g i)} →
          [inst : (i : I) → DistribMulAction (f i) (g i)] → DistribMulAction ((i : I) → f i) ((i : I) → g i)
distribMulAction' {g: I → Type ?u.18834
g : I: Type u
I → Type _: Type (?u.18834+1)
Type _} {m: (i : I) → Monoid (f i)
m : ∀ i: ?m.18838
i, Monoid: Type ?u.18841 → Type ?u.18841
Monoid (f: I → Type v
f i: ?m.18838
i)} {n: (i : I) → AddMonoid (g i)
n : ∀ i: ?m.18845
i, AddMonoid: Type ?u.18848 → Type ?u.18848
AddMonoid <| g: I → Type ?u.18834
g i: ?m.18845
i}
    [∀ i: ?m.18852
i, DistribMulAction: (M : Type ?u.18856) → (A : Type ?u.18855) → [inst : Monoid M] → [inst : AddMonoid A] → Type (max?u.18856?u.18855)
DistribMulAction (f: I → Type v
f i: ?m.18852
i) (g: I → Type ?u.18834
g i: ?m.18852
i)] :
    @DistribMulAction: (M : Type ?u.18885) → (A : Type ?u.18884) → [inst : Monoid M] → [inst : AddMonoid A] → Type (max?u.18885?u.18884)
DistribMulAction (∀ i: ?m.18887
i, f: I → Type v
f i: ?m.18887
i) (∀ i: I
i : I: Type u
I, g: I → Type ?u.18834
g i: I
i) (@Pi.monoid: {I : Type ?u.18896} → {f : I → Type ?u.18895} → [inst : (i : I) → Monoid (f i)] → Monoid ((i : I) → f i)
Pi.monoid I: Type u
I f: I → Type v
f m: (i : I) → Monoid (f i)
m) (@Pi.addMonoid: {I : Type ?u.18905} → {f : I → Type ?u.18904} → [inst : (i : I) → AddMonoid (f i)] → AddMonoid ((i : I) → f i)
Pi.addMonoid I: Type u
I g: I → Type ?u.18834
g n: (i : I) → AddMonoid (g i)
n) :=
  { Pi.mulAction', Pi.distribSMul' with }: DistribMulAction ?m.19032 ?m.19033
{ Pi.mulAction': {I : Type ?u.18924} →
  {f : I → Type ?u.18923} →
    {g : I → Type ?u.18922} →
      {m : (i : I) → Monoid (f i)} →
        [inst : (i : I) → MulAction (f i) (g i)] → MulAction ((i : I) → f i) ((i : I) → g i)
Pi.mulAction'{ Pi.mulAction', Pi.distribSMul' with }: DistribMulAction ?m.19032 ?m.19033
, Pi.distribSMul': {I : Type ?u.18984} →
  {f : I → Type ?u.18983} →
    {g : I → Type ?u.18982} →
      {n : (i : I) → AddZeroClass (g i)} →
        [inst : (i : I) → DistribSMul (f i) (g i)] → DistribSMul ((i : I) → f i) ((i : I) → g i)
Pi.distribSMul'{ Pi.mulAction', Pi.distribSMul' with }: DistribMulAction ?m.19032 ?m.19033
 { Pi.mulAction', Pi.distribSMul' with }: DistribMulAction ?m.19032 ?m.19033
with{ Pi.mulAction', Pi.distribSMul' with }: DistribMulAction ?m.19032 ?m.19033
 }
#align pi.distrib_mul_action' Pi.distribMulAction': {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {m : (i : I) → Monoid (f i)} →
        {n : (i : I) → AddMonoid (g i)} →
          [inst : (i : I) → DistribMulAction (f i) (g i)] → DistribMulAction ((i : I) → f i) ((i : I) → g i)
Pi.distribMulAction'

theorem single_smul: ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : (i : I) → AddMonoid (f i)] [inst_2 : (i : I) → DistribMulAction α (f i)]
  [inst_3 : DecidableEq I] (i : I) (r : α) (x : f i), single i (r • x) = r • single i x
single_smul {α: ?m.21046
α} [Monoid: Type ?u.21049 → Type ?u.21049
Monoid α: ?m.21046
α] [∀ i: ?m.21053
i, AddMonoid: Type ?u.21056 → Type ?u.21056
AddMonoid <| f: I → Type v
f i: ?m.21053
i] [∀ i: ?m.21061
i, DistribMulAction: (M : Type ?u.21065) → (A : Type ?u.21064) → [inst : Monoid M] → [inst : AddMonoid A] → Type (max?u.21065?u.21064)
DistribMulAction α: ?m.21046
α <| f: I → Type v
f i: ?m.21061
i]
    [DecidableEq: Sort ?u.21089 → Sort (max1?u.21089)
DecidableEq I: Type u
I] (i: I
i : I: Type u
I) (r: α
r : α: ?m.21046
α) (x: f i
x : f: I → Type v
f i: I
i) : single: {I : Type ?u.21106} →
  {f : I → Type ?u.21105} → [inst : DecidableEq I] → [inst : (i : I) → Zero (f i)] → (i : I) → f i → (j : I) → f j
single i: I
i (r: α
r • x: f i
x) = r: α
r • single: {I : Type ?u.22058} →
  {f : I → Type ?u.22057} → [inst : DecidableEq I] → [inst : (i : I) → Zero (f i)] → (i : I) → f i → (j : I) → f j
single i: I
i x: f i
x :=
  single_op: ∀ {I : Type ?u.22853} {f : I → Type ?u.22852} [inst : DecidableEq I] [inst_1 : (i : I) → Zero (f i)]
  {g : I → Type ?u.22854} [inst_2 : (i : I) → Zero (g i)] (op : (i : I) → f i → g i),
  (∀ (i : I), op i 0 = 0) → ∀ (i : I) (x : f i), single i (op i x) = fun j => op j (single i x j)
single_op (fun i: I
i : I: Type u
I => ((· • ·): α → f i → f i
(· • ·) r: α
r : f: I → Type v
f i: I
i → f: I → Type v
f i: I
i)) (fun _: ?m.23004
_ => smul_zero: ∀ {M : Type ?u.23007} {A : Type ?u.23006} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0
smul_zero _: ?m.23008
_) _: ?m.22855
_ _: ?m.22856 ?m.24592
_
#align pi.single_smul Pi.single_smul: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : Monoid α] [inst_1 : (i : I) → AddMonoid (f i)]
  [inst_2 : (i : I) → DistribMulAction α (f i)] [inst_3 : DecidableEq I] (i : I) (r : α) (x : f i),
  single i (r • x) = r • single i x
Pi.single_smul

-- Porting note: Lean4 cannot infer the non-dependent function `f := fun _ => β`
/-- A version of `Pi.single_smul` for non-dependent functions. It is useful in cases where Lean
fails to apply `Pi.single_smul`. -/
theorem single_smul': ∀ {I : Type u} {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : AddMonoid β] [inst_2 : DistribMulAction α β]
  [inst_3 : DecidableEq I] (i : I) (r : α) (x : β), single i (r • x) = r • single i x
single_smul' {α: Type u_1
α β: ?m.24970
β} [Monoid: Type ?u.24973 → Type ?u.24973
Monoid α: ?m.24967
α] [AddMonoid: Type ?u.24976 → Type ?u.24976
AddMonoid β: ?m.24970
β] [DistribMulAction: (M : Type ?u.24980) → (A : Type ?u.24979) → [inst : Monoid M] → [inst : AddMonoid A] → Type (max?u.24980?u.24979)
DistribMulAction α: ?m.24967
α β: ?m.24970
β] [DecidableEq: Sort ?u.24999 → Sort (max1?u.24999)
DecidableEq I: Type u
I] (i: I
i : I: Type u
I)
    (r: α
r : α: ?m.24967
α) (x: β
x : β: ?m.24970
β) : single: {I : Type ?u.25016} →
  {f : I → Type ?u.25015} → [inst : DecidableEq I] → [inst : (i : I) → Zero (f i)] → (i : I) → f i → (j : I) → f j
single (f := fun _: ?m.25019
_ => β: ?m.24970
β) i: I
i (r: α
r • x: β
x) = r: α
r • single: {I : Type ?u.26100} →
  {f : I → Type ?u.26099} → [inst : DecidableEq I] → [inst : (i : I) → Zero (f i)] → (i : I) → f i → (j : I) → f j
single (f := fun _: ?m.26103
_ => β: ?m.24970
β) i: I
i x: β
x :=
  single_smul: ∀ {I : Type ?u.27689} {f : I → Type ?u.27688} {α : Type ?u.27690} [inst : Monoid α] [inst_1 : (i : I) → AddMonoid (f i)]
  [inst_2 : (i : I) → DistribMulAction α (f i)] [inst_3 : DecidableEq I] (i : I) (r : α) (x : f i),
  single i (r • x) = r • single i x
single_smul (f := fun _: ?m.27693
_ => β: Type u_2
β) i: I
i r: α
r x: β
x
#align pi.single_smul' Pi.single_smul': ∀ {I : Type u} {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : AddMonoid β] [inst_2 : DistribMulAction α β]
  [inst_3 : DecidableEq I] (i : I) (r : α) (x : β), single i (r • x) = r • single i x
Pi.single_smul'

theorem single_smul₀: ∀ {g : I → Type u_1} [inst : (i : I) → MonoidWithZero (f i)] [inst_1 : (i : I) → AddMonoid (g i)]
  [inst_2 : (i : I) → DistribMulAction (f i) (g i)] [inst_3 : DecidableEq I] (i : I) (r : f i) (x : g i),
  single i (r • x) = single i r • single i x
single_smul₀ {g: I → Type ?u.27847
g : I: Type u
I → Type _: Type (?u.27847+1)
Type _} [∀ i: ?m.27851
i, MonoidWithZero: Type ?u.27854 → Type ?u.27854
MonoidWithZero (f: I → Type v
f i: ?m.27851
i)] [∀ i: ?m.27859
i, AddMonoid: Type ?u.27862 → Type ?u.27862
AddMonoid (g: I → Type ?u.27847
g i: ?m.27859
i)]
    [∀ i: ?m.27867
i, DistribMulAction: (M : Type ?u.27871) → (A : Type ?u.27870) → [inst : Monoid M] → [inst : AddMonoid A] → Type (max?u.27871?u.27870)
DistribMulAction (f: I → Type v
f i: ?m.27867
i) (g: I → Type ?u.27847
g i: ?m.27867
i)] [DecidableEq: Sort ?u.27908 → Sort (max1?u.27908)
DecidableEq I: Type u
I] (i: I
i : I: Type u
I) (r: f i
r : f: I → Type v
f i: I
i) (x: g i
x : g: I → Type ?u.27847
g i: I
i) :
    single: {I : Type ?u.27925} →
  {f : I → Type ?u.27924} → [inst : DecidableEq I] → [inst : (i : I) → Zero (f i)] → (i : I) → f i → (j : I) → f j
single i: I
i (r: f i
r • x: g i
x) = single: {I : Type ?u.28959} →
  {f : I → Type ?u.28958} → [inst : DecidableEq I] → [inst : (i : I) → Zero (f i)] → (i : I) → f i → (j : I) → f j
single i: I
i r: f i
r • single: {I : Type ?u.29137} →
  {f : I → Type ?u.29136} → [inst : DecidableEq I] → [inst : (i : I) → Zero (f i)] → (i : I) → f i → (j : I) → f j
single i: I
i x: g i
x :=
  single_op₂: ∀ {I : Type ?u.30036} {f : I → Type ?u.30035} [inst : DecidableEq I] [inst_1 : (i : I) → Zero (f i)]
  {g₁ : I → Type ?u.30037} {g₂ : I → Type ?u.30038} [inst_2 : (i : I) → Zero (g₁ i)] [inst_3 : (i : I) → Zero (g₂ i)]
  (op : (i : I) → g₁ i → g₂ i → f i),
  (∀ (i : I), op i 0 0 = 0) →
    ∀ (i : I) (x₁ : g₁ i) (x₂ : g₂ i), single i (op i x₁ x₂) = fun j => op j (single i x₁ j) (single i x₂ j)
single_op₂ (fun i: I
i : I: Type u
I => ((· • ·): f i → g i → g i
(· • ·) : f: I → Type v
f i: I
i → g: I → Type u_1
g i: I
i → g: I → Type u_1
g i: I
i)) (fun _: ?m.30458
_ => smul_zero: ∀ {M : Type ?u.30461} {A : Type ?u.30460} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0
smul_zero _: ?m.30462
_) _: ?m.30039
_ _: ?m.30043 ?m.31341
_ _: ?m.30044 ?m.31341
_
#align pi.single_smul₀ Pi.single_smul₀: ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} [inst : (i : I) → MonoidWithZero (f i)]
  [inst_1 : (i : I) → AddMonoid (g i)] [inst_2 : (i : I) → DistribMulAction (f i) (g i)] [inst_3 : DecidableEq I]
  (i : I) (r : f i) (x : g i), single i (r • x) = single i r • single i x
Pi.single_smul₀

instance mulDistribMulAction: {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) →
      {m : Monoid α} →
        {n : (i : I) → Monoid (f i)} →
          [inst : (i : I) → MulDistribMulAction α (f i)] → MulDistribMulAction α ((i : I) → f i)
mulDistribMulAction (α: Type ?u.31542
α) {m: Monoid α
m : Monoid: Type ?u.31542 → Type ?u.31542
Monoid α: ?m.31539
α} {n: (i : I) → Monoid (f i)
n : ∀ i: ?m.31546
i, Monoid: Type ?u.31549 → Type ?u.31549
Monoid <| f: I → Type v
f i: ?m.31546
i}
    [∀ i: ?m.31553
i, MulDistribMulAction: (M : Type ?u.31557) → (A : Type ?u.31556) → [inst : Monoid M] → [inst : Monoid A] → Type (max?u.31557?u.31556)
MulDistribMulAction α: ?m.31539
α <| f: I → Type v
f i: ?m.31553
i] :
    @MulDistribMulAction: (M : Type ?u.31585) → (A : Type ?u.31584) → [inst : Monoid M] → [inst : Monoid A] → Type (max?u.31585?u.31584)
MulDistribMulAction α: ?m.31539
α (∀ i: I
i : I: Type u
I, f: I → Type v
f i: I
i) m: Monoid α
m (@Pi.monoid: {I : Type ?u.31591} → {f : I → Type ?u.31590} → [inst : (i : I) → Monoid (f i)] → Monoid ((i : I) → f i)
Pi.monoid I: Type u
I f: I → Type v
f n: (i : I) → Monoid (f i)
n) :=
  { Pi.mulAction: {I : Type ?u.31609} →
  {f : I → Type ?u.31608} →
    (α : Type ?u.31607) → {m : Monoid α} → [inst : (i : I) → MulAction α (f i)] → MulAction α ((i : I) → f i)
Pi.mulAction _: Type ?u.31607
_ with
    smul_one := fun _: ?m.31990
_ => funext: ∀ {α : Sort ?u.31993} {β : α → Sort ?u.31992} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun _: ?m.32003
_ => smul_one: ∀ {M : Type ?u.32006} {A : Type ?u.32005} [inst : Monoid M] [inst_1 : Monoid A] [self : MulDistribMulAction M A]
  (r : M), r • 1 = 1
smul_one _: ?m.32007
_
    smul_mul := fun _: ?m.31793
_ _: ?m.31796
_ _: ?m.31799
_ => funext: ∀ {α : Sort ?u.31802} {β : α → Sort ?u.31801} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun _: ?m.31813
_ => smul_mul': ∀ {M : Type ?u.31816} {A : Type ?u.31815} [inst : Monoid M] [inst_1 : Monoid A] [inst_2 : MulDistribMulAction M A]
  (a : M) (b₁ b₂ : A), a • (b₁ * b₂) = a • b₁ * a • b₂
smul_mul' _: ?m.31817
_ _: ?m.31818
_ _: ?m.31818
_ }
#align pi.mul_distrib_mul_action Pi.mulDistribMulAction: {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) →
      {m : Monoid α} →
        {n : (i : I) → Monoid (f i)} →
          [inst : (i : I) → MulDistribMulAction α (f i)] → MulDistribMulAction α ((i : I) → f i)
Pi.mulDistribMulAction

instance mulDistribMulAction': {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {m : (i : I) → Monoid (f i)} →
        {n : (i : I) → Monoid (g i)} →
          [inst : (i : I) → MulDistribMulAction (f i) (g i)] → MulDistribMulAction ((i : I) → f i) ((i : I) → g i)
mulDistribMulAction' {g: I → Type ?u.32275
g : I: Type u
I → Type _: Type (?u.32275+1)
Type _} {m: (i : I) → Monoid (f i)
m : ∀ i: ?m.32279
i, Monoid: Type ?u.32282 → Type ?u.32282
Monoid (f: I → Type v
f i: ?m.32279
i)} {n: (i : I) → Monoid (g i)
n : ∀ i: ?m.32286
i, Monoid: Type ?u.32289 → Type ?u.32289
Monoid <| g: I → Type ?u.32275
g i: ?m.32286
i}
    [∀ i: ?m.32293
i, MulDistribMulAction: (M : Type ?u.32297) → (A : Type ?u.32296) → [inst : Monoid M] → [inst : Monoid A] → Type (max?u.32297?u.32296)
MulDistribMulAction (f: I → Type v
f i: ?m.32293
i) (g: I → Type ?u.32275
g i: ?m.32293
i)] :
    @MulDistribMulAction: (M : Type ?u.32329) → (A : Type ?u.32328) → [inst : Monoid M] → [inst : Monoid A] → Type (max?u.32329?u.32328)
MulDistribMulAction (∀ i: ?m.32331
i, f: I → Type v
f i: ?m.32331
i) (∀ i: I
i : I: Type u
I, g: I → Type ?u.32275
g i: I
i) (@Pi.monoid: {I : Type ?u.32340} → {f : I → Type ?u.32339} → [inst : (i : I) → Monoid (f i)] → Monoid ((i : I) → f i)
Pi.monoid I: Type u
I f: I → Type v
f m: (i : I) → Monoid (f i)
m) (@Pi.monoid: {I : Type ?u.32349} → {f : I → Type ?u.32348} → [inst : (i : I) → Monoid (f i)] → Monoid ((i : I) → f i)
Pi.monoid I: Type u
I g: I → Type ?u.32275
g n: (i : I) → Monoid (g i)
n) where
  smul_mul := by
Goals accomplished! 🐙
    I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.32275

m: (i : I) → Monoid (f i)

n: (i : I) → Monoid (g i)

inst✝: (i : I) → MulDistribMulAction (f i) (g i)

∀ (r : (i : I) → f i) (x y : (i : I) → g i), r • (x * y) = r • x * r • yintrosI: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.32275

m: (i : I) → Monoid (f i)

n: (i : I) → Monoid (g i)

inst✝: (i : I) → MulDistribMulAction (f i) (g i)

r✝: (i : I) → f i

x✝, y✝: (i : I) → g i

r✝ • (x✝ * y✝) = r✝ • x✝ * r✝ • y✝
    I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.32275

m: (i : I) → Monoid (f i)

n: (i : I) → Monoid (g i)

inst✝: (i : I) → MulDistribMulAction (f i) (g i)

∀ (r : (i : I) → f i) (x y : (i : I) → g i), r • (x * y) = r • x * r • yext x: ?α
xI: Type u

f: I → Type v

x✝¹, y: (i : I) → f i

i: I

g: I → Type ?u.32275

m: (i : I) → Monoid (f i)

n: (i : I) → Monoid (g i)

inst✝: (i : I) → MulDistribMulAction (f i) (g i)

r✝: (i : I) → f i

x✝, y✝: (i : I) → g i

x: I

h(r✝ • (x✝ * y✝)) x = (r✝ • x✝ * r✝ • y✝) x
    I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.32275

m: (i : I) → Monoid (f i)

n: (i : I) → Monoid (g i)

inst✝: (i : I) → MulDistribMulAction (f i) (g i)

∀ (r : (i : I) → f i) (x y : (i : I) → g i), r • (x * y) = r • x * r • yapply smul_mul': ∀ {M : Type ?u.32621} {A : Type ?u.32620} [inst : Monoid M] [inst_1 : Monoid A] [inst_2 : MulDistribMulAction M A]
  (a : M) (b₁ b₂ : A), a • (b₁ * b₂) = a • b₁ * a • b₂
smul_mul'
Goals accomplished! 🐙
  smul_one := by
Goals accomplished! 🐙
    I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.32275

m: (i : I) → Monoid (f i)

n: (i : I) → Monoid (g i)

inst✝: (i : I) → MulDistribMulAction (f i) (g i)

∀ (r : (i : I) → f i), r • 1 = 1introsI: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.32275

m: (i : I) → Monoid (f i)

n: (i : I) → Monoid (g i)

inst✝: (i : I) → MulDistribMulAction (f i) (g i)

r✝: (i : I) → f i

r✝ • 1 = 1
    I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.32275

m: (i : I) → Monoid (f i)

n: (i : I) → Monoid (g i)

inst✝: (i : I) → MulDistribMulAction (f i) (g i)

∀ (r : (i : I) → f i), r • 1 = 1ext x: ?α
xI: Type u

f: I → Type v

x✝, y: (i : I) → f i

i: I

g: I → Type ?u.32275

m: (i : I) → Monoid (f i)

n: (i : I) → Monoid (g i)

inst✝: (i : I) → MulDistribMulAction (f i) (g i)

r✝: (i : I) → f i

x: I

h(r✝ • 1) x = OfNat.ofNat 1 x
    I: Type u

f: I → Type v

x, y: (i : I) → f i

i: I

g: I → Type ?u.32275

m: (i : I) → Monoid (f i)

n: (i : I) → Monoid (g i)

inst✝: (i : I) → MulDistribMulAction (f i) (g i)

∀ (r : (i : I) → f i), r • 1 = 1apply smul_one: ∀ {M : Type ?u.32715} {A : Type ?u.32714} [inst : Monoid M] [inst_1 : Monoid A] [self : MulDistribMulAction M A]
  (r : M), r • 1 = 1
smul_one
Goals accomplished! 🐙
#align pi.mul_distrib_mul_action' Pi.mulDistribMulAction': {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {m : (i : I) → Monoid (f i)} →
        {n : (i : I) → Monoid (g i)} →
          [inst : (i : I) → MulDistribMulAction (f i) (g i)] → MulDistribMulAction ((i : I) → f i) ((i : I) → g i)
Pi.mulDistribMulAction'

end Pi

namespace Function

/-- Non-dependent version of `Pi.smul`. Lean gets confused by the dependent instance if this
is not present. -/
@[to_additive: {ι : Type u_1} → {R : Type u_2} → {M : Type u_3} → [inst : VAdd R M] → VAdd R (ι → M)
to_additive
  "Non-dependent version of `Pi.vadd`. Lean gets confused by the dependent instance
  if this is not present."]
instance hasSMul: {ι : Type u_1} → {R : Type u_2} → {M : Type u_3} → [inst : SMul R M] → SMul R (ι → M)
hasSMul {ι: Type ?u.32945
ι R: Type ?u.32948
R M: Type ?u.32951
M : Type _: Type (?u.32951+1)
Type _} [SMul: Type ?u.32955 → Type ?u.32954 → Type (max?u.32955?u.32954)
SMul R: Type ?u.32948
R M: Type ?u.32951
M] : SMul: Type ?u.32959 → Type ?u.32958 → Type (max?u.32959?u.32958)
SMul R: Type ?u.32948
R (ι: Type ?u.32945
ι → M: Type ?u.32951
M) :=
  Pi.instSMul: {I : Type ?u.32971} →
  {α : Type ?u.32969} → {f : I → Type ?u.32970} → [inst : (i : I) → SMul α (f i)] → SMul α ((i : I) → f i)
Pi.instSMul
#align function.has_smul Function.hasSMul: {ι : Type u_1} → {R : Type u_2} → {M : Type u_3} → [inst : SMul R M] → SMul R (ι → M)
Function.hasSMul
#align function.has_vadd Function.hasVAdd: {ι : Type u_1} → {R : Type u_2} → {M : Type u_3} → [inst : VAdd R M] → VAdd R (ι → M)
Function.hasVAdd

/-- Non-dependent version of `Pi.smulCommClass`. Lean gets confused by the dependent instance if
this is not present. -/
@[to_additive: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [inst : VAdd α M] [inst_1 : VAdd β M]
  [inst_2 : VAddCommClass α β M], VAddCommClass α β (ι → M)
to_additive
  "Non-dependent version of `Pi.vaddCommClass`. Lean gets confused by the dependent
  instance if this is not present."]
instance smulCommClass: ∀ {ι : Type ?u.33191} {α : Type ?u.33194} {β : Type ?u.33197} {M : Type ?u.33200} [inst : SMul α M] [inst_1 : SMul β M]
  [inst_2 : SMulCommClass α β M], SMulCommClass α β (ι → M)
smulCommClass {ι: Type ?u.33191
ι α: Type ?u.33194
α β: Type ?u.33197
β M: Type ?u.33200
M : Type _: Type (?u.33191+1)
Type _} [SMul: Type ?u.33204 → Type ?u.33203 → Type (max?u.33204?u.33203)
SMul α: Type ?u.33194
α M: Type ?u.33200
M] [SMul: Type ?u.33208 → Type ?u.33207 → Type (max?u.33208?u.33207)
SMul β: Type ?u.33197
β M: Type ?u.33200
M] [SMulCommClass: (M : Type ?u.33213) → (N : Type ?u.33212) → (α : Type ?u.33211) → [inst : SMul M α] → [inst : SMul N α] → Prop
SMulCommClass α: Type ?u.33194
α β: Type ?u.33197
β M: Type ?u.33200
M] :
    SMulCommClass: (M : Type ?u.33240) → (N : Type ?u.33239) → (α : Type ?u.33238) → [inst : SMul M α] → [inst : SMul N α] → Prop
SMulCommClass α: Type ?u.33194
α β: Type ?u.33197
β (ι: Type ?u.33191
ι → M: Type ?u.33200
M) :=
  Pi.smulCommClass: ∀ {I : Type ?u.33346} {f : I → Type ?u.33345} {α : Type ?u.33344} {β : Type ?u.33343} [inst : (i : I) → SMul α (f i)]
  [inst_1 : (i : I) → SMul β (f i)] [inst_2 : ∀ (i : I), SMulCommClass α β (f i)], SMulCommClass α β ((i : I) → f i)
Pi.smulCommClass
#align function.smul_comm_class Function.smulCommClass: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [inst : SMul α M] [inst_1 : SMul β M]
  [inst_2 : SMulCommClass α β M], SMulCommClass α β (ι → M)
Function.smulCommClass
#align function.vadd_comm_class Function.vaddCommClass: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [inst : VAdd α M] [inst_1 : VAdd β M]
  [inst_2 : VAddCommClass α β M], VAddCommClass α β (ι → M)
Function.vaddCommClass

@[to_additive: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → VAdd α (f i)] [inst_1 : DecidableEq I] (c : α)
  (f₁ : (i : I) → f i) (i : I) (x₁ : f i), update (c +ᵥ f₁) i (c +ᵥ x₁) = c +ᵥ update f₁ i x₁
to_additive]
theorem update_smul: ∀ {α : Type u_1} [inst : (i : I) → SMul α (f i)] [inst_1 : DecidableEq I] (c : α) (f₁ : (i : I) → f i) (i : I)
  (x₁ : f i), update (c • f₁) i (c • x₁) = c • update f₁ i x₁
update_smul {α: Type u_1
α : Type _: Type (?u.33688+1)
Type _} [∀ i: ?m.33692
i, SMul: Type ?u.33696 → Type ?u.33695 → Type (max?u.33696?u.33695)
SMul α: Type ?u.33688
α (f: I → Type v
f i: ?m.33692
i)] [DecidableEq: Sort ?u.33700 → Sort (max1?u.33700)
DecidableEq I: Type u
I] (c: α
c : α: Type ?u.33688
α) (f₁: (i : I) → f i
f₁ : ∀ i: ?m.33712
i, f: I → Type v
f i: ?m.33712
i)
    (i: I
i : I: Type u
I) (x₁: f i
x₁ : f: I → Type v
f i: I
i) : update: {α : Sort ?u.33723} →
  {β : α → Sort ?u.33722} → [inst : DecidableEq α] → ((a : α) → β a) → (a' : α) → β a' → (a : α) → β a
update (c: α
c • f₁: (i : I) → f i
f₁) i: I
i (c: α
c • x₁: f i
x₁) = c: α
c • update: {α : Sort ?u.33882} →
  {β : α → Sort ?u.33881} → [inst : DecidableEq α] → ((a : α) → β a) → (a' : α) → β a' → (a : α) → β a
update f₁: (i : I) → f i
f₁ i: I
i x₁: f i
x₁ :=
  funext: ∀ {α : Sort ?u.34010} {β : α → Sort ?u.34009} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun j: ?m.34024
j => (apply_update: ∀ {ι : Sort ?u.34026} [inst : DecidableEq ι] {α : ι → Sort ?u.34027} {β : ι → Sort ?u.34028} (f : (i : ι) → α i → β i)
  (g : (i : ι) → α i) (i : ι) (v : α i) (j : ι), f j (update g i v j) = update (fun k => f k (g k)) i (f i v) j
apply_update (β := f: I → Type v
f) (fun _: ?m.34036
_ => (· • ·): α → f x✝ → f x✝
(· • ·) c: α
c) f₁: (i : I) → f i
f₁ i: I
i x₁: f i
x₁ j: ?m.34024
j).symm: ∀ {α : Sort ?u.34207} {a b : α}, a = b → b = a
symm
#align function.update_smul Function.update_smul: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → SMul α (f i)] [inst_1 : DecidableEq I] (c : α)
  (f₁ : (i : I) → f i) (i : I) (x₁ : f i), update (c • f₁) i (c • x₁) = c • update f₁ i x₁
Function.update_smul
#align function.update_vadd Function.update_vadd: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → VAdd α (f i)] [inst_1 : DecidableEq I] (c : α)
  (f₁ : (i : I) → f i) (i : I) (x₁ : f i), update (c +ᵥ f₁) i (c +ᵥ x₁) = c +ᵥ update f₁ i x₁
Function.update_vadd

end Function

namespace Set

@[to_additive: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → VAdd α (f i)] (s : Set I)
  [inst_1 : (i : I) → Decidable (i ∈ s)] (c : α) (f₁ g₁ : (i : I) → f i),
  piecewise s (c +ᵥ f₁) (c +ᵥ g₁) = c +ᵥ piecewise s f₁ g₁
to_additive]
theorem piecewise_smul: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → SMul α (f i)] (s : Set I)
  [inst_1 : (i : I) → Decidable (i ∈ s)] (c : α) (f₁ g₁ : (i : I) → f i),
  piecewise s (c • f₁) (c • g₁) = c • piecewise s f₁ g₁
piecewise_smul {α: Type u_1
α : Type _: Type (?u.34500+1)
Type _} [∀ i: ?m.34504
i, SMul: Type ?u.34508 → Type ?u.34507 → Type (max?u.34508?u.34507)
SMul α: Type ?u.34500
α (f: I → Type v
f i: ?m.34504
i)] (s: Set I
s : Set: Type ?u.34512 → Type ?u.34512
Set I: Type u
I) [∀ i: ?m.34516
i, Decidable: Prop → Type
Decidable (i: ?m.34516
i ∈ s: Set I
s)]
    (c: α
c : α: Type ?u.34500
α) (f₁: (i : I) → f i
f₁ g₁: (i : I) → f i
g₁ : ∀ i: ?m.34543
i, f: I → Type v
f i: ?m.34543
i) : s: Set I
s.piecewise: {α : Type ?u.34556} →
  {β : α → Sort ?u.34555} →
    (s : Set α) → ((i : α) → β i) → ((i : α) → β i) → [inst : (j : α) → Decidable (j ∈ s)] → (i : α) → β i
piecewise (c: α
c • f₁: (i : I) → f i
f₁) (c: α
c • g₁: (i : I) → f i
g₁) = c: α
c • s: Set I
s.piecewise: {α : Type ?u.34734} →
  {β : α → Sort ?u.34733} →
    (s : Set α) → ((i : α) → β i) → ((i : α) → β i) → [inst : (j : α) → Decidable (j ∈ s)] → (i : α) → β i
piecewise f₁: (i : I) → f i
f₁ g₁: (i : I) → f i
g₁ :=
  s: Set I
s.piecewise_op: ∀ {α : Type ?u.34820} {δ : α → Sort ?u.34821} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)]
  {δ' : α → Sort ?u.34819} (h : (i : α) → δ i → δ' i),
  (piecewise s (fun x => h x (f x)) fun x => h x (g x)) = fun x => h x (piecewise s f g x)
piecewise_op (δ' := f: I → Type v
f) f₁: (i : I) → f i
f₁ _: (i : ?m.34830) → ?m.34831 i
_ fun _: ?m.34857
_ => (· • ·): α → f x✝ → f x✝
(· • ·) c: α
c
#align set.piecewise_smul Set.piecewise_smul: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → SMul α (f i)] (s : Set I)
  [inst_1 : (i : I) → Decidable (i ∈ s)] (c : α) (f₁ g₁ : (i : I) → f i),
  piecewise s (c • f₁) (c • g₁) = c • piecewise s f₁ g₁
Set.piecewise_smul
#align set.piecewise_vadd Set.piecewise_vadd: ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : (i : I) → VAdd α (f i)] (s : Set I)
  [inst_1 : (i : I) → Decidable (i ∈ s)] (c : α) (f₁ g₁ : (i : I) → f i),
  piecewise s (c +ᵥ f₁) (c +ᵥ g₁) = c +ᵥ piecewise s f₁ g₁
Set.piecewise_vadd

end Set

section Extend

@[to_additive: ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd R γ] (r : R) (f : α → β) (g : α → γ)
  (e : β → γ), extend f (r +ᵥ g) (r +ᵥ e) = r +ᵥ extend f g e
to_additive]
theorem Function.extend_smul: ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul R γ] (r : R) (f : α → β) (g : α → γ)
  (e : β → γ), extend f (r • g) (r • e) = r • extend f g e
Function.extend_smul {R: Type u_1
R α: Type ?u.35279
α β: Type ?u.35282
β γ: Type ?u.35285
γ : Type _: Type (?u.35279+1)
Type _} [SMul: Type ?u.35289 → Type ?u.35288 → Type (max?u.35289?u.35288)
SMul R: Type ?u.35276
R γ: Type ?u.35285
γ] (r: R
r : R: Type ?u.35276
R) (f: α → β
f : α: Type ?u.35279
α → β: Type ?u.35282
β) (g: α → γ
g : α: Type ?u.35279
α → γ: Type ?u.35285
γ)
    (e: β → γ
e : β: Type ?u.35282
β → γ: Type ?u.35285
γ) : Function.extend: {α : Sort ?u.35309} → {β : Sort ?u.35308} → {γ : Sort ?u.35307} → (α → β) → (α → γ) → (β → γ) → β → γ
Function.extend f: α → β
f (r: R
r • g: α → γ
g) (r: R
r • e: β → γ
e) = r: R
r • Function.extend: {α : Sort ?u.35479} → {β : Sort ?u.35478} → {γ : Sort ?u.35477} → (α → β) → (α → γ) → (β → γ) → β → γ
Function.extend f: α → β
f g: α → γ
g e: β → γ
e :=
  funext: ∀ {α : Sort ?u.35565} {β : α → Sort ?u.35564} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun x: ?m.35579
x => by
Goals accomplished! 🐙
  -- Porting note: Lean4 is unable to automatically call `Classical.propDecidable`
  I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

extend f (r • g) (r • e) x = (r • extend f g e) xhaveI : Decidable: Prop → Type
Decidable (∃ a: α
a : α: Type u_2
α, f: α → β
f a: α
a = x: β
x) := Classical.propDecidable: (a : Prop) → Decidable a
Classical.propDecidable _: Prop
_I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

extend f (r • g) (r • e) x = (r • extend f g e) x
  I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

extend f (r • g) (r • e) x = (r • extend f g e) xrw [I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

extend f (r • g) (r • e) x = (r • extend f g e) xextend_def: ∀ {α : Sort ?u.35603} {β : Sort ?u.35604} {γ : Sort ?u.35605} (f : α → β) (g : α → γ) (e' : β → γ) (b : β)
  [inst : Decidable (∃ a, f a = b)], extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b
extend_def,I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

(if h : ∃ a, f a = x then (r • g) (Classical.choose h) else (r • e) x) = (r • extend f g e) x I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

extend f (r • g) (r • e) x = (r • extend f g e) xPi.smul_apply: ∀ {I : Type ?u.35657} {β : Type ?u.35658} {f : I → Type ?u.35656} [inst : (i : I) → SMul β (f i)] (b : β)
  (x : (i : I) → f i) (i : I), (b • x) i = b • x i
Pi.smul_apply,I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

(if h : ∃ a, f a = x then (r • g) (Classical.choose h) else r • e x) = (r • extend f g e) x I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

extend f (r • g) (r • e) x = (r • extend f g e) xPi.smul_apply: ∀ {I : Type ?u.35779} {β : Type ?u.35780} {f : I → Type ?u.35778} [inst : (i : I) → SMul β (f i)] (b : β)
  (x : (i : I) → f i) (i : I), (b • x) i = b • x i
Pi.smul_apply,I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

(if h : ∃ a, f a = x then (r • g) (Classical.choose h) else r • e x) = r • extend f g e x I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

extend f (r • g) (r • e) x = (r • extend f g e) xextend_def: ∀ {α : Sort ?u.35864} {β : Sort ?u.35865} {γ : Sort ?u.35866} (f : α → β) (g : α → γ) (e' : β → γ) (b : β)
  [inst : Decidable (∃ a, f a = b)], extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b
extend_defI: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

(if h : ∃ a, f a = x then (r • g) (Classical.choose h) else r • e x) =   r • if h : ∃ a, f a = x then g (Classical.choose h) else e x]I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

(if h : ∃ a, f a = x then (r • g) (Classical.choose h) else r • e x) =   r • if h : ∃ a, f a = x then g (Classical.choose h) else e x
  I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

extend f (r • g) (r • e) x = (r • extend f g e) xsplit_ifsI: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

h✝: ∃ a, f a = x

inl(r • g) (Classical.choose h✝) = r • g (Classical.choose h✝)
I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

h✝: ¬∃ a, f a = x

inrr • e x = r • e x I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

(if h : ∃ a, f a = x then (r • g) (Classical.choose h) else r • e x) =   r • if h : ∃ a, f a = x then g (Classical.choose h) else e x<;>I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

h✝: ∃ a, f a = x

inl(r • g) (Classical.choose h✝) = r • g (Classical.choose h✝)
I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

h✝: ¬∃ a, f a = x

inrr • e x = r • e x
  I: Type u

f✝: I → Type v

x✝, y: (i : I) → f✝ i

i: I

R: Type u_1

α: Type u_2

β: Type u_3

γ: Type u_4

inst✝: SMul R γ

r: R

f: α → β

g: α → γ

e: β → γ

x: β

this: Decidable (∃ a, f a = x)

(if h : ∃ a, f a = x then (r • g) (Classical.choose h) else r • e x) =   r • if h : ∃ a, f a = x then g (Classical.choose h) else e xrfl
Goals accomplished! 🐙
  -- convert (apply_dite (fun c : γ => r • c) _ _ _).symm
#align function.extend_smul Function.extend_smul: ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul R γ] (r : R) (f : α → β) (g : α → γ)
  (e : β → γ), Function.extend f (r • g) (r • e) = r • Function.extend f g e
Function.extend_smul
#align function.extend_vadd Function.extend_vadd: ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd R γ] (r : R) (f : α → β) (g : α → γ)
  (e : β → γ), Function.extend f (r +ᵥ g) (r +ᵥ e) = r +ᵥ Function.extend f g e
Function.extend_vadd

end Extend