no goals
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type ?u.466820
inst✝² : Monoid N
inst✝¹ : (i : ι) → DecidableEq (M i)
inst✝ : DecidableEq ι
m : FreeProduct M
⊢ ∀ (w : Word M), prod (m • w) = m * prod w
induction m using FreeProduct.induction_on with
| h_one =>
  intro
  rw [one_smul, one_mul]
| h_of _ =>
  intros
  rw [of_smul_def, prod_rcons, of.map_mul, mul_assoc, ← prod_rcons, ← equivPair_symm,
    Equiv.symm_apply_apply]
| h_mul x y hx hy =>
  intro w
  rw [mul_smul, hx, hy, mul_assoc]
case h_one
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type ?u.466820
inst✝² : Monoid N
inst✝¹ : (i : ι) → DecidableEq (M i)
inst✝ : DecidableEq ι
w✝ : Word M
⊢ prod (1 • w✝) = 1 * prod w✝
case h_one
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type ?u.466820
inst✝² : Monoid N
inst✝¹ : (i : ι) → DecidableEq (M i)
inst✝ : DecidableEq ι
⊢ ∀ (w : Word M), prod (1 • w) = 1 * prod w
intro
no goals
case h_one
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type ?u.466820
inst✝² : Monoid N
inst✝¹ : (i : ι) → DecidableEq (M i)
inst✝ : DecidableEq ι
w✝ : Word M
⊢ prod (1 • w✝) = 1 * prod w✝
rw [one_smul, one_mul]
case h_of
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type ?u.466820
inst✝² : Monoid N
inst✝¹ : (i : ι) → DecidableEq (M i)
inst✝ : DecidableEq ι
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ prod (↑of m✝ • w✝) = ↑of m✝ * prod w✝
case h_of
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type ?u.466820
inst✝² : Monoid N
inst✝¹ : (i : ι) → DecidableEq (M i)
inst✝ : DecidableEq ι
i✝ : ι
m✝ : M i✝
⊢ ∀ (w : Word M), prod (↑of m✝ • w) = ↑of m✝ * prod w
intros
no goals
case h_of
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type ?u.466820
inst✝² : Monoid N
inst✝¹ : (i : ι) → DecidableEq (M i)
inst✝ : DecidableEq ι
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ prod (↑of m✝ • w✝) = ↑of m✝ * prod w✝
rw [of_smul_def, prod_rcons, of.map_mul, mul_assoc, ← prod_rcons, ← equivPair_symm,
  Equiv.symm_apply_apply]
case h_mul
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type ?u.466820
inst✝² : Monoid N
inst✝¹ : (i : ι) → DecidableEq (M i)
inst✝ : DecidableEq ι
x y : FreeProduct M
hx : ∀ (w : Word M), prod (x • w) = x * prod w
hy : ∀ (w : Word M), prod (y • w) = y * prod w
w : Word M
⊢ prod ((x * y) • w) = x * y * prod w
case h_mul
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type ?u.466820
inst✝² : Monoid N
inst✝¹ : (i : ι) → DecidableEq (M i)
inst✝ : DecidableEq ι
x y : FreeProduct M
hx : ∀ (w : Word M), prod (x • w) = x * prod w
hy : ∀ (w : Word M), prod (y • w) = y * prod w
⊢ ∀ (w : Word M), prod ((x * y) • w) = x * y * prod w
intro w
no goals
case h_mul
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type ?u.466820
inst✝² : Monoid N
inst✝¹ : (i : ι) → DecidableEq (M i)
inst✝ : DecidableEq ι
x y : FreeProduct M
hx : ∀ (w : Word M), prod (x • w) = x * prod w
hy : ∀ (w : Word M), prod (y • w) = y * prod w
w : Word M
⊢ prod ((x * y) • w) = x * y * prod w
rw [mul_smul, hx, hy, mul_assoc]