ι : Type u_1
α : Type ?u.28780
M : Type u_3
N : Type u_4
P : Type u_2
M₀ : Type ?u.28792
G : Type ?u.28795
R : Type ?u.28798
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ foldl (fun x y => x * f (f₁ y) (f₂ y)) 1 l = f (foldl (fun x y => x * f₁ y) 1 l) (foldl (fun x y => x * f₂ y) 1 l)
ι : Type u_1
α : Type ?u.28780
M : Type u_3
N : Type u_4
P : Type u_2
M₀ : Type ?u.28792
G : Type ?u.28795
R : Type ?u.28798
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ prod (map (fun i => f (f₁ i) (f₂ i)) l) = f (prod (map f₁ l)) (prod (map f₂ l))
simp only [prod, foldl_map]
case h
ι : Type u_1
α : Type ?u.28780
M : Type u_3
N : Type u_4
P : Type u_2
M₀ : Type ?u.28792
G : Type ?u.28795
R : Type ?u.28798
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ ∀ (a : M) (b : N) (i : ι), f (a * f₁ i) (b * f₂ i) = f a b * f (f₁ i) (f₂ i)
ι : Type u_1
α : Type ?u.28780
M : Type u_3
N : Type u_4
P : Type u_2
M₀ : Type ?u.28792
G : Type ?u.28795
R : Type ?u.28798
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ foldl (fun x y => x * f (f₁ y) (f₂ y)) 1 l = f (foldl (fun x y => x * f₁ y) 1 l) (foldl (fun x y => x * f₂ y) 1 l)
rw [← l.foldl_hom₂ (fun a b => f a b), hf']
case h
ι : Type u_1
α : Type ?u.28780
M : Type u_3
N : Type u_4
P : Type u_2
M₀ : Type ?u.28792
G : Type ?u.28795
R : Type ?u.28798
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
a✝ : M
b✝ : N
i✝ : ι
⊢ f (a✝ * f₁ i✝) (b✝ * f₂ i✝) = f a✝ b✝ * f (f₁ i✝) (f₂ i✝)
case h
ι : Type u_1
α : Type ?u.28780
M : Type u_3
N : Type u_4
P : Type u_2
M₀ : Type ?u.28792
G : Type ?u.28795
R : Type ?u.28798
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ ∀ (a : M) (b : N) (i : ι), f (a * f₁ i) (b * f₂ i) = f a b * f (f₁ i) (f₂ i)
intros
no goals
case h
ι : Type u_1
α : Type ?u.28780
M : Type u_3
N : Type u_4
P : Type u_2
M₀ : Type ?u.28792
G : Type ?u.28795
R : Type ?u.28798
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
a✝ : M
b✝ : N
i✝ : ι
⊢ f (a✝ * f₁ i✝) (b✝ * f₂ i✝) = f a✝ b✝ * f (f₁ i✝) (f₂ i✝)
exact hf _ _ _ _