Theorem: Function.HasTemperateGrowth.prod (ForML/HasTemperateGrowth.lean)

State before:
ι : Type u_1
inst✝⁴ : DecidableEq ι
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Finset ι
f : ι → E → ℝ
hf : ∀ i ∈ s, HasTemperateGrowth (f i)
⊢ HasTemperateGrowth fun x => ∏ i in s, f i x
Tactic:
induction s using Finset.induction with
| empty => simp [hasTemperateGrowth_const]
| @insert i s hi IH =>
  simp only [Finset.mem_insert, forall_eq_or_imp] at hf
  simpa [Finset.prod_insert hi] using HasTemperateGrowth.mul hf.1 (IH hf.2)
State after:
no goals

State before:
case empty
ι : Type u_1
inst✝⁴ : DecidableEq ι
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ι → E → ℝ
hf : ∀ i ∈ ∅, HasTemperateGrowth (f i)
⊢ HasTemperateGrowth fun x => ∏ i in ∅, f i x
Tactic:
simp [hasTemperateGrowth_const]
State after:
no goals

State before:
case insert
ι : Type u_1
inst✝⁴ : DecidableEq ι
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ι → E → ℝ
i : ι
s : Finset ι
hi : i ∉ s
IH : (∀ i ∈ s, HasTemperateGrowth (f i)) → HasTemperateGrowth fun x => ∏ i in s, f i x
hf : ∀ i_1 ∈ insert i s, HasTemperateGrowth (f i_1)
⊢ HasTemperateGrowth fun x => ∏ i in insert i s, f i x
Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at hf
State after:
case insert
ι : Type u_1
inst✝⁴ : DecidableEq ι
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ι → E → ℝ
i : ι
s : Finset ι
hi : i ∉ s
IH : (∀ i ∈ s, HasTemperateGrowth (f i)) → HasTemperateGrowth fun x => ∏ i in s, f i x
hf : HasTemperateGrowth (f i) ∧ ∀ a ∈ s, HasTemperateGrowth (f a)
⊢ HasTemperateGrowth fun x => ∏ i in insert i s, f i x

State before:
case insert
ι : Type u_1
inst✝⁴ : DecidableEq ι
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ι → E → ℝ
i : ι
s : Finset ι
hi : i ∉ s
IH : (∀ i ∈ s, HasTemperateGrowth (f i)) → HasTemperateGrowth fun x => ∏ i in s, f i x
hf : HasTemperateGrowth (f i) ∧ ∀ a ∈ s, HasTemperateGrowth (f a)
⊢ HasTemperateGrowth fun x => ∏ i in insert i s, f i x
Tactic:
simpa [Finset.prod_insert hi] using HasTemperateGrowth.mul hf.1 (IH hf.2)
State after:
no goals