case nil
α : Type u_1
β : Type u_2
γ : Type ?u.34343
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : Monoid β
l : List (α → β)
hl✝ : ∀ (f : α → β), f ∈ l → Periodic f c
hl : ∀ (f : α → β), f ∈ [] → Periodic f c
⊢ Periodic (List.prod []) c

case cons
α : Type u_1
β : Type u_2
γ : Type ?u.34343
f g✝ : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : Monoid β
l✝ : List (α → β)
hl✝ : ∀ (f : α → β), f ∈ l✝ → Periodic f c
g : α → β
l : List (α → β)
ih : (∀ (f : α → β), f ∈ l → Periodic f c) → Periodic (List.prod l) c
hl : ∀ (f : α → β), f ∈ g :: l → Periodic f c
⊢ Periodic (List.prod (g :: l)) c
α : Type u_1
β : Type u_2
γ : Type ?u.34343
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : Monoid β
l : List (α → β)
hl : ∀ (f : α → β), f ∈ l → Periodic f c
⊢ Periodic (List.prod l) c
induction' l with g l ih hl
no goals
case nil
α : Type u_1
β : Type u_2
γ : Type ?u.34343
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : Monoid β
l : List (α → β)
hl✝ : ∀ (f : α → β), f ∈ l → Periodic f c
hl : ∀ (f : α → β), f ∈ [] → Periodic f c
⊢ Periodic (List.prod []) c
simp
case cons
α : Type u_1
β : Type u_2
γ : Type ?u.34343
f g✝ : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : Monoid β
l✝ : List (α → β)
hl✝ : ∀ (f : α → β), f ∈ l✝ → Periodic f c
g : α → β
l : List (α → β)
ih : (∀ (f : α → β), f ∈ l → Periodic f c) → Periodic (List.prod l) c
hl : Periodic g c ∧ ∀ (x : α → β), x ∈ l → Periodic x c
⊢ Periodic (List.prod (g :: l)) c
case cons
α : Type u_1
β : Type u_2
γ : Type ?u.34343
f g✝ : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : Monoid β
l✝ : List (α → β)
hl✝ : ∀ (f : α → β), f ∈ l✝ → Periodic f c
g : α → β
l : List (α → β)
ih : (∀ (f : α → β), f ∈ l → Periodic f c) → Periodic (List.prod l) c
hl : ∀ (f : α → β), f ∈ g :: l → Periodic f c
⊢ Periodic (List.prod (g :: l)) c
rw [List.forall_mem_cons] at hl
no goals
case cons
α : Type u_1
β : Type u_2
γ : Type ?u.34343
f g✝ : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : Monoid β
l✝ : List (α → β)
hl✝ : ∀ (f : α → β), f ∈ l✝ → Periodic f c
g : α → β
l : List (α → β)
ih : (∀ (f : α → β), f ∈ l → Periodic f c) → Periodic (List.prod l) c
hl : Periodic g c ∧ ∀ (x : α → β), x ∈ l → Periodic x c
⊢ Periodic (List.prod (g :: l)) c
simpa only [List.prod_cons] using hl.1.mul (ih hl.2)